Zulip Chat Archive

Stream: general

Topic: Notation trouble


Alice Laroche (Jan 01 2022 at 20:15):

I have trouble to get a notation working,
Basically i have this, and i get invalid expression starting at 7:25, can someone help me solve this ?

inductive term
| T
open term

inductive reduction : term -> term -> term -> term -> Prop
notation A ` ~ ` B `  ` j `  ` j' := reduction A B j j'
| beta   : A B: term, A ~ B  T  T

Reid Barton (Jan 01 2022 at 20:40):

I think it's because is reserved notation. It works for me if I change that to, say, ~>.

Alice Laroche (Jan 01 2022 at 20:45):

Thanks, i replaced it by

Patrick Johnson (Jan 01 2022 at 20:47):

You can disable prelude and then use , but it is not recommended:

prelude
abbreviation Prop := Sort 0

inductive term
| T
open term

inductive reduction : term -> term -> term -> term -> Prop
notation A ` ~ ` B `  ` j `  ` j' := reduction A B j j'
| beta   : A B: term, A ~ B  T  T

Alice Laroche (Jan 01 2022 at 20:48):

Yeah no, disabling the prelude is not the solution


Last updated: Dec 20 2023 at 11:08 UTC