Zulip Chat Archive

Stream: new members

Topic: reserving notation


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 16 2021 at 17:17):

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

view this post on Zulip Eric Wieser (Mar 16 2021 at 17:18):

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

view this post on Zulip Horatiu Cheval (Mar 16 2021 at 17:20):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 16 2021 at 17:30):

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

view this post on Zulip 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