Write a function to find the last entry in a list

Stream: new members

[Adolfo Neto]

Hi,

I am trying to solve the Exercises in

https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#exercises

The first one is "Write a function to find the last entry in a list. It should return an Option."

Is this a good solution?

def last {α  : Type} (xs : List α) : Option α :=
  match xs with
  | [] => none
  | ls :: []  => some ls
  | _ :: tail => last (tail)

#eval last [1,2,3]
#eval last [1,2]
#eval last [1]
#eval last (α := Int) []

[Kyle Miller]

Looks good to me.

Just changing the syntax a little, you could also write this as

def last {α : Type} (xs : List α) : Option α :=
  match xs with
  | [] => none
  | [ls] => some ls
  | _ :: tail => last tail

[Kyle Miller]

Here's another style you might see:

def last {α : Type} : List α → Option α
  | [] => none
  | [ls] => some ls
  | _ :: tail => last tail

It's completely equivalent.

[Adolfo Neto]

Thanks, @Kyle Miller!

[Adolfo Neto]

To use last with an empty list, do I really have to add (α := Int)?

[Eric Wieser]

You can also write last ([] : List Int)

[Adolfo Neto]

Thanks, @Eric Wieser!