theorem_proving_in_lean4
theorem_proving_in_lean4 copied to clipboard
Published
20 hours ago •
leanprover
leanprover
These 2 sentences in Ch. 7 are a holdover from Lean3
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 |.
per the discussion here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Basic.20question.20about.20inductive.20types
