Implicit type in dependent types

Stream: new members

[Roey Hel-Or]

Hi, newbie here.

I'm trying to define an inductive dependent type:

variable {α : Type} [LinearOrder α]

inductive Tree : Type
| leaf : Tree
| node (value : α) (left : Tree) (right : Tree) : Tree
deriving Repr

I can easily make an example instance and evaluate it
def example_tree := Tree.node 1 Tree.leaf Tree.leaf
#eval example_tree -- Tree.node 1 (Tree.leaf) (Tree.leaf)

However when trying to implement a new function dependent on this type I get a message
def is_heap : Tree → Prop
| Tree.leaf => true
| Tree.node v l r =>
(match l with
| Tree.leaf => true
| Tree.node lv _ _ => lv ≤ v )
∧ (match r with
| Tree.leaf => true
| Tree.node rv _ _ => rv ≤ v)
∧ is_heap l
∧ is_heap r

don't know how to synthesize implicit argument
@Tree ?m.1202
context:
α: Type
inst✝: LinearOrder α
⊢ Type

when the resulting type of a declaration is explicitly provided, all holes (e.g., _) in the header are resolved before the declaration body is processed.

What is the problem?

[Roey Hel-Or]

Neither this syntax work: def is_heap (t : Tree) : Prop :=

Or this one as well: def is_heap (t : Tree α) : Prop :=
(Error now is:
function expected at
Tree
term has type
Type
)

[Kyle Miller]

It would be better to make α be an explicit variable to Tree, since otherwise Lean can't really figure out what this argument should be.

[Kyle Miller]

note: #backticks

[Kyle Miller]

For example, set up your type with

variable (α : Type) [LinearOrder α]

inductive Tree : Type
  | leaf : Tree
  | node (value : α) (left : Tree) (right : Tree) : Tree
  deriving Repr

variable {α}

That then makes α be implicit afterwards.