using infix in definition

Stream: general

[Minchao Wu]

I remember that in Lean 2 we could use infix inside a definition, referring to the thing being defined.
Is this implemented in the latest master branch?

[Mario Carneiro]

I don't think there is anything like that

[Sebastian Ullrich]

inductive sub : env → type → type → Prop
  notation e ` ⊢ `:40 a ` <: `:40 b:40 := sub e a b
| ...

[Sebastian Ullrich]

The only change is the removal of := after the type

[Minchao Wu]

Worked for me! Thanks Sebastian and Mario.

[Mario Carneiro]

Wait, does that work for def as well? I thought it only worked in inductive and structure

[Minchao Wu]

My bad, I should have said inductive definitions