## Stream: new members

### Topic: infix notation

#### 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 -/


#### Kyle Miller (Sep 16 2020 at 06:40):

How is similar M defined?

#### 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


#### 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)

#### Michael Beeson (Sep 16 2020 at 06:59):

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

#### Kyle Miller (Sep 16 2020 at 07:03):

(Greetings from Berkeley :smile:)

Last updated: May 16 2021 at 05:21 UTC