Use notation for type in type definition itself

Stream: new members

[kana]

set_option quotPrecheck false
infix:50 " ⟶ " => eval
inductive eval : Nat → Nat → Prop where
| zero_zero : 0 ⟶ 0

Unexpected resulting type for constructor `eval.zero_zero`: Expected an application of
  eval
but found
  0 ⟶ 0

The only workaround I know is to generate type definition via macro

[Kenny Lau]

@kana

set_option hygiene false
infix:50 " ⟶ " => eval

inductive eval : Nat → Nat → Prop where
| zero_zero : 0 ⟶ 0

#print eval

[suhr]

(off-topic) Hello, Kana.