inductive def

Stream: general

[Patrick Massot]

I very rarely use inductive def so I'm a bit confused by:

-- Works ok
def find : ℕ → list ℕ → bool
| a []     := ff
| a (h::t) := if (a = h) then tt else find a t

-- Lean complains: type mismatch at application  find' a, term  a has type  ℕ but is expected to have type   list ℕ
def find' (a : ℕ) : list ℕ → bool
| []     := ff
| (h::t) := if (a = h) then tt else find' a t

Is there a way to get something like my second attempt to work?

[Gabriel Ebner]

find' t (without the a)

[Gabriel Ebner]

(The parameters before the colon---a in this case---are assumed to be constant in the recursive calls, so you don't have to repeat them.)

[Kevin Buzzard]

That used to confuse me so much.

inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a

I was like "...yeah, but what is a equal to??". It's equal to the a before the colon.

[Patrick Massot]

Thanks!