Func Prog in Lean Linked List code not working 1.6.1

Stream: lean4

[Damias McDonald]

Define list of primes for n less than 10:

def primesUnder10 : List Nat := [2, 3, 5, 7]

Tried to use length definition but couldn't get it to work with similar error messages.

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length α ys)

and

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length α ys)

Get error:

FuncProgBook.lean:232:26

Expected type
⊢ Type

Messages (1)

FuncProgBook.lean:232:13

application type mismatch
length primesUnder10
argument
primesUnder10
has type
List Nat : Type
but is expected to have type
Type : Type 1

All Messages (52)

[Henrik Böving]

What exactly is "1.6.1" referring to here? The code you posted just works on current Lean versions, see e.g. here

[Ilmārs Cīrulis]

This works:

def primesUnder10 : List Nat := [2, 3, 5, 7]

def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length ys)

#eval length primesUnder10

[Damias McDonald]

Henrik Böving said:

What exactly is "1.6.1" referring to here? The code you posted just works on current Lean versions, see e.g. here

I'm referring to section 1.6.1 in the book Functional Programming in Lean

[Aaron Liu]

you want to provide the α argument

[Ilmārs Cīrulis]

Or, if you don't like the implicit argument

def primesUnder10 : List Nat := [2, 3, 5, 7]

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length _ ys)

#eval length _ primesUnder10

[Damias McDonald]

Ilmārs Cīrulis said:

This works:

def primesUnder10 : List Nat := [2, 3, 5, 7]

def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length ys)

#eval length primesUnder10

Yes, the implicite one works, but I'm trying to figure out why the other don't even though they're listed as working solutions in the book.

[Ilmārs Cīrulis]

If you don't make it implicit, then at least an underscore for it must be provided.

[Ilmārs Cīrulis]

Underscore then is "filled" by Lean, because it deduces the value of α from the type of the list.

[Damias McDonald]

Gotcha, thanks for letting me know! That makes a lot of sense.

[Kenny Lau]

the error message also tells you that it's expecting a type but you fed it a list