infix notation

Stream: new members

[Michael Beeson]

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]

How is similar M defined?

[Kyle Miller]

There's also this sort of approach for notation:

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

[Kyle Miller]

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]

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

[Kyle Miller]

(Greetings from Berkeley :smile:)