Zulip Chat Archive

Stream: new members

Topic: Problem 2.10 "Theorem Proving in Lean"

view this post on Zulip Christopher Sumnicht (Jan 19 2019 at 01:31):

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.

view this post on Zulip Mario Carneiro (Jan 19 2019 at 01:40):

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

Last updated: May 12 2021 at 05:19 UTC