theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
leanprover
Theorem Proving in Lean 4
Hi, Working through the book and loving it. Thanks. Quick question on In the section **Propositional Logic** we have > So if we have ``p q r : Prop``, the...
These examples in Chapter 7, Inductive Types raise recursion depth errors: ``` namespace Hidden theorem add_zero (n : Nat) : n + 0 = n := Nat.add_zero n open Nat...
I looked into this a bit and filed an issue here https://github.com/leanprover-community/highlightjs-lean/issues/19. We may need to update our version of highlight-js, as it does seem to mark `mutual` as a...
Error "unknown identifier 'hp'" in chapter 3 "Propositions and Proofs" when using `variable (hp: p)`
# Description Lean gives the error "unknown identifier 'hp'" when I put [this example code](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#working-with-propositions-as-types) into an otherwise empty file: ```lean variable {p q : Prop} variable (hp : p)...
Could be it possible to have the PDF version of this tutorial accessible without using print this book?
It is quite difficult to navigate back and forth without the table of contents, considering that the book is written in 12 big one-page chapters. This PR uses `mdbook-toc` to...
Ch. 6, section "Using the Library" has the following broken link: [https://github.com/leanprover-community/batteries/tree/main/Std](https://github.com/leanprover-community/batteries/tree/main/Std)
The following from Ch. 7 should be deleted: > The first character | in an inductive declaration is optional. We can also separate constructors using a comma instead of |....
