theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
leanprover
Theorem Proving in Lean 4
Hi, I am reading _Theorem Proving in Lean 4_ on VSCodium. I have installed the common lean4 extension. But some graphics is missing as evidences by this picture?  I...
In newer lean versions, the divisibility symbol $\mid$ (`\mid`) is already defined, hence ```lean infix:50 " ∣ " => divides example (h₁ : divides x y) (h₂ : y =...
Using `rw [Nat.add_comm b]` should change ``a + (b + c)`` to ``a + (c + b)`` instead. See: https://live.lean-lang.org/#code=example%20(a%20b%20c%20%3A%20Nat)%20%3A%20a%20%2B%20b%20%2B%20c%20%3D%20a%20%2B%20c%20%2B%20b%20%3A%3D%20by%0A%20%20rw%20%5BNat.add_assoc%2C%20Nat.add_comm%20b%2C%20←%20Nat.add_assoc%5D
These changes allow the tests to pass with the latest Lean nightly again.
Unlike other Lean documentation, such as Functional Programming in Lean, theme changes every time I click on the print icon. I have tried to print the document with Microsoft Edge...
The section Auto Bound Implicit Arguments (in chapter 6 Interacting with Lean) says >When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit...
There are two instances of Section Local Recursive Declarations in induction_and_recursion.md. This pull request removes the second one (at the end of the file).
I recently tried to search for how to introduce a `let` expression, but got no results. It would be nice if the search functionality would return hits to lean keywords...
Two issues, If you use the code as written it doesn't have the right type for Trans, also there's a clash with the existing | operator
Dear all, In Propositions and Proofs, when the `suffices` keyword is introduced, the text reads, "Writing ``suffices hq : q`` leaves us with two goals.". I was expecting, in the...
