reserving notation

Stream: new members

[Horatiu Cheval]

Can I define a notation before defining the notion it is intended to stand for, so that I may use the notation starting from the very first definition? So, instead of this

inductive my_eq {α : Type} : α → α → Type
| my_refl : ∀ x : α, my_eq x x

infix `≅` : 50 := my_eq

define the notation first, and the write \congr instead of my_eq in the constructor

[Eric Wieser]

I tried using let notation `≅` : 50 in ... in that definition, but it doesn't seem there's anywhere its legal

[Eric Wieser]

inductive my_eq {α : Type} : α → α → Type
| my_refl : let infix `≅` : 50 := my_eq in ∀ (x : α), x ≅ x

[Eric Wieser]

Although you have to repeat it for every constructor, which probably isn't what you wanted

[Horatiu Cheval]

Wow, nice, I never thought something like that could be legal syntax

[Horatiu Cheval]

I see, I remembered that Coq had a way to this, so I figured there might be an equivalent for Lean.

[Horatiu Cheval]

Like here, on the "Evaluation as Relation" section,
you basically reserve the notation, and specify what it refers to only after the definition

[Eric Wieser]

You could maybe ask in the #lean4 stream for whether there will be notation for this

[Eric Wieser]

Perhaps after glancing at the lean4 docs first