Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC