Notation trouble

Stream: general

[Alice Laroche]

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]

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

[Alice Laroche]

Thanks, i replaced it by ▹

[Patrick Johnson]

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]

Yeah no, disabling the prelude is not the solution