theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
leanprover
Theorem Proving in Lean 4
Defining the `Implies` function whilst hiding it from the rendered document makes following the chapter difficult, as the reader expects that it is a built-in alongside the other propositional connectives....
In "Function Abstraction and Evaluation", the examples of function abstractions where the Nat argument is documented as being inferred are in fact not: `λ x: Nat => x + 5`...
In https://lean-lang.org/theorem_proving_in_lean4/type_classes.html I noticed an error. In the 5th example part of it states: ``` #eval double (10 : Int) -- 100 ``` However, the actual evaluation returns 10 as-is....
Sorry, I ignore the hint in the `( )`. I think it would be more easier to catch if just put the hint in the code like other exercises. For...
In Chapter 6 Interacting with Lean under **Using the Library**, the link in the second bullet leads to a page that is not available.
Users who actually try the examples in VS Code will be confused when a comment disagrees with what they see when they hover. I think the first such example is...
https://github.com/leanprover/theorem_proving_in_lean4/blob/ee6aeb4f1db92c3fed2121944bdd1d4871d6d851/propositions_and_proofs.md?plain=1#L36-L38 It has brought some confusion https://stackoverflow.com/questions/69182724/lean-4-unknown-identifier-proof . People may also try the code on their editor.
Add links to FPiL and the metaprogramming book. Fixes #28. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/add.20links.20to.20other.20lean.20tutorials.20to.20tpil4
This book doesn't mention this coercion, I think we should write it explicitly.
The next few lines show that there should be an implicit parameter