Problem 2.10 "Theorem Proving in Lean"

Stream: new members

[Christopher Sumnicht]

Hello, I hope this is the correct place to ask this. I was looking at the Theorem Proving in Lean book exercises in Chap 2 which asks to both add two vectors together and reverse a vector. I have the following questions:

1. Why does it want to make a constant instead of a definition?
2. Normally, I would pattern match in Haskell on the head and tail of a list to solve both problems, but I don't know how to do this without recursion (as recursion isn't mentioned until later in chap 8). Any hints as to how to do this without recursion would be appreciated.

[Mario Carneiro]

Normally we would define that as a function, but this is early in the book and the question is only about getting the type right. For the exercise you aren't even trying to make the definition itself, just the type of the hypothetical definition