Coq-like notation with inductive

Stream: Is there code for X?

[Zhuanhao Wu]

I'm wondering if I can use coq like inductive notation as follows for aevalR. I'm trying to find a way that allows me to use ==> within the definition of aevalR inductive

import Mathlib

namespace AExp

inductive aexp where
| ANum   (n: ℕ)
deriving Repr

-- set_option quotPrecheck false in
-- notation:90 e:90 "==>" n:89 => aevalR e n

inductive aevalR: aexp -> ℕ -> Prop where
| E_Anum (n: ℕ): (ANum n) ==> n
where e "==>" n := aevalR e n  -- this won't work of course


end AExp

[Shreyas Srinivas]

Maybe this helps: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Does.20.60set_option.20hygiene.20false.60.20not.20work.20with.20.60notation3.60.3F/near/455228084

[Zhuanhao Wu]

Thank you, I think it is the one I'm looking for, and the following works for me

import Mathlib

namespace AExp

inductive aexp where
| ANum   (n: ℕ)

deriving Repr

set_option hygiene false

-- set_option quotPrecheck false in
notation:90 e:90 "==>" n:89 => aevalR e n


inductive aevalR: aexp -> ℕ -> Prop where
| E_Anum (n: ℕ): (.ANum n) ==> n
-- where e "==>" n := aevalR e n


end AExp

[Shreyas Srinivas]

import Mathlib

namespace AExp

inductive aexp where
| ANum   (n: ℕ)

deriving Repr

section Temp

set_option hygiene false

-- set_option quotPrecheck false in
local notation:90 e:90 "==>" n:89 => aevalR e n


inductive aevalR: aexp -> ℕ -> Prop where
| E_Anum (n: ℕ): (.ANum n) ==> n
-- where e "==>" n := aevalR e n
end Temp

notation:90 e:90 "==>" n:89 => aevalR e n

end AExp

[Shreyas Srinivas]

This way you also get unexpanders for your notation

[Zhuanhao Wu]

Nice, thanks for the info

[Kyle Miller]

It's also how you can make sure ==> will always refer to the correct aevalR, even if another aevalR is in scope. This is what hygiene is for.