theorem_proving_in_lean
theorem_proving_in_lean copied to clipboard
Remove outdated syntax information
Reported at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/syntax.20of.20inductive.20definitions .
Hm, I just stumbled across this, too. It is also in the Lean 4 version of Theorem Proving in Lean.