search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

7.5 Other Recursive Data Types #95

Closed vvs- closed 4 years ago

vvs- commented 4 years ago

It seems that this section has introduced too much without explanation. I thought that this tutorial assumed not much background about Lean or functional programming.

In the first example it used list.rec while there was no real explanation of its syntax and semantics. After introducing recursors first in 7.1 it quickly switched to rec_on without elaborating on their differences. There are no explanations here either, the reader will rely on guesses and experiments.

Then it introduces iterative notation without ever explaining what that syntax do or what foldr function means. And it might be only guessed that it's actually a function at all.

That was actually a first time I was so puzzled reading this book as it was otherwise very smooth up to this point. And thanks for a good reading anyway.

avigad commented 4 years ago

Thanks for the feedback. We are not planning and substantial additions or changes to TPIL right now, but this may be useful for a future addition. In the meanwhile, I recommend stopping by the Zulip channel: https://leanprover.zulipchat.com/. There is a friendly community there happy to answer questions.