theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
leanprover
Theorem Proving in Lean 4
I noticed this while learning lean through the documentation. The declaration of `tp` seems like a typo to me.
I was going through the chapter on tactics and noticed what looks like a minor copy/paste redundancy.
While running `mdbook test` across my local fork so I could create a PR, I noticed there are many errors reported.
It seems that there are two different notations for anonymous constructors: ``` instance : ToString Rules := { toString := fun rs => "TBD" } ``` and ``` instance :...
The link for "Programming in Lean 4" is broken in These aspects of Lean are explored in a companion tutorial to this one, Programming in Lean 4, though computational aspects...
# Dependent Type Theory ## Function Abstraction and Evaluation There is a statement "...has nothing to do with the constant ``b`` declared earlier." but there is no such declaration of...
Looks like it was moved, please check that this is correct because I haven't seen the old one.
