search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
156 stars 83 forks source link

Maybe it is worth emphasizing that Proof is not a built-in type #57

Open zxch3n opened 1 year ago

zxch3n commented 1 year ago

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.

pimotte commented 1 year ago

Same holds for Implies, which I ran into. I do get the educational lie, it reads nicely this way. I don't really see how to communicate this properly without interrupting the flow of text.