## Stream: new members

### Topic: reserving notation

#### Horatiu Cheval (Mar 16 2021 at 17:08):

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 (Mar 16 2021 at 17:16):

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

#### Eric Wieser (Mar 16 2021 at 17:17):

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


#### Eric Wieser (Mar 16 2021 at 17:18):

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

#### Horatiu Cheval (Mar 16 2021 at 17:20):

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

#### Horatiu Cheval (Mar 16 2021 at 17:22):

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

#### Horatiu Cheval (Mar 16 2021 at 17:25):

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 (Mar 16 2021 at 17:30):

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

#### Eric Wieser (Mar 16 2021 at 17:30):

Perhaps after glancing at the lean4 docs first

Last updated: May 11 2021 at 00:31 UTC