The answer by Meven Lennon-Bertrand is exactly right, but the best way to ensure you are doing structural recursion is to avoid writing the match statement in the first place:

def zip {α β : Type} : (as: List α) -> (bs: List β) -> List (α × β)
| a::arest, b::brest => (a, b) :: zip arest brest
| _, _ => []

While it is no more than semantic sugar for Meven’s answer, it is, I would say, more idiomatic for Lean. (Also I labeled the parameters as and bs, but that isn’t needed.)

Also maybe it is worth making an issue about your example on the Lean GitHub. It seems that Lean could make this compile or at least provide a better error message, since I think that will be a common user mistake since it is the way matching on two variables is done in some other functional languages.

The answer by Meven Lennon-Bertrand is exactly right, but the best way to ensure you are doing structural recursion is to avoid writing the match statement in the first place:

def zip {α β : Type} : (as: List α) -> (bs: List β) -> List (α × β)
| a::arest, b::brest => (a, b) :: zip arest brest
| _, _ => []

While it is no more than semantic sugar for Meven’s answer, it is, I would say, more idiomatic for Lean. (Also I labeled the parameters as and bs, but that isn’t needed.)

Also maybe it is worth making an issue about your example on the Lean GitHub. It seems that Lean could make this compile or at least provide a better error message, since I think that will be a common user mistake since it is the way recursive functions matching on two variables are done in some other functional languages.