Zulip Chat Archive

Stream: new members

Topic: infix notation


view this post on Zulip Michael Beeson (Sep 16 2020 at 06:29):

I am working with a class Model and an instance M of that class. Then I define an equivalence relation similar M. That is, in every
instance M of model it will be an equivalence relation. I would like to write x ~ y instead of (similar M x y). But since similar takes three
arguments I can't seem to do it. Of course for relations that are defined inside the class itself, like \subseteq, there is no problem,
but I can't define similar inside the class as I must first define some other things that are used in the definition of similar. Most of my
definitions are outside the class so every definition and lemma and theorem has an "extra" M tagging along. I've gotten used to that
but if it's possible to write x ~y instead of (similar M x y), please tell me how. Here's a test example of a class.

class  Model (M:Type) :=
(𝔽:M)
(succ:M)
(Λ:M)
(mem : M  M  Prop)
(infix   :=  mem )
(SSC: M  M)
(emptyset_axiom:    x, (¬ x  Λ ))
 /- end of class definition because next line doesn't declare a member -/

view this post on Zulip Kyle Miller (Sep 16 2020 at 06:40):

How is similar M defined?

view this post on Zulip Kyle Miller (Sep 16 2020 at 06:42):

There's also this sort of approach for notation:

notation x `~[`M`]` y := similar M x y

view this post on Zulip Kyle Miller (Sep 16 2020 at 06:46):

But, since Model is a class, something like this might work:

abbreviation similar' {M : Type} [Model M] (x y : M) : Prop := similar M x y
infix `~` := similar'

(you might want to modify similar itself so that M is an implicit variable like this)

view this post on Zulip Michael Beeson (Sep 16 2020 at 06:59):

Thanks, I will try this tomorrow. (it's midnight now in California).

view this post on Zulip Kyle Miller (Sep 16 2020 at 07:03):

(Greetings from Berkeley :smile:)


Last updated: May 16 2021 at 05:21 UTC