mlocal_fresh

Stream: new members

[Horatiu Cheval]

Can I explicitly give a name to types of x and y in the recursive definition instead of the autogenerated __mlocal__fresh... in order to use them later in the equation? (Like case can do in tactic mode)

inductive ty: Type 0 → Type 1
| comp : ∀ {α β : Type}, ty α → ty β → ty (α → β)

def f : ∀ {α : Type}, ty α → α
| α (ty.comp x y) := _

[Alex J. Best]

You can use @ to make the types explicit and match on them

inductive ty: Type 0 → Type 1
| comp : ∀ {α β : Type}, ty α → ty β → ty (α → β)
open ty
def f : ∀ {α : Type}, ty α → α
| α (@comp a b x y) := _

[Horatiu Cheval]

Thanks!