theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
leanprover
Theorem Proving in Lean 4
In the chapter induction and recursion, part "dependant pattern matching", I find the explanations quite hard to follow. First, the goal of the auxiliairy functions is not described explicitely Worse,...
Suggestions to clarify some possibly confusing items. Main ones are: - Introducing arguments in a way consistent with the idea that functions really only take one argument at a time...
The below code from the Quantifiers and Equality chapter gives an "ambiguous, possible interpretations" error for this line: ```x ∣ y := h₁``` you can see it if you paste...
The file induction_and_recursion.md has two sections titled "Local recursive declarations". It looks like it was [moved from one place to another](https://github.com/leanprover/theorem_proving_in_lean4/commit/b877fef75226d0f155f5b2fe6c1c6c3863e60b9f) on March 3, 2022 and then it was [restored...
The tactics chapter states that > In the first example, the left branch succeeds, whereas in the second one, it is the right one that succeeds. > In the next...
As noted on Zulip, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/experiment.20making.20.60succ_eq_add_one.60.20.40.5Bsimp.5D.60/near/446392853.
Hi, I've added a way to render the book as pdf, together with a generated copy. The underlying dependency requires a Chrome-like browser to be installed for PDF rendering. Let...
This pull request responds to the request from Bulhwi Cha to clarify that Lean's core library is not committed to avoiding classical: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/constructive.20tactic.20mode.20in.20lean/near/431736331 The previous wording dates back to the...