theorem_proving_in_lean icon indicating copy to clipboard operation
theorem_proving_in_lean copied to clipboard

Remove outdated syntax information

Open digama0 opened this issue 4 years ago • 1 comments

Reported at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/syntax.20of.20inductive.20definitions .

digama0 avatar Dec 10 '21 18:12 digama0

Hm, I just stumbled across this, too. It is also in the Lean 4 version of Theorem Proving in Lean.

abentkamp avatar May 26 '23 11:05 abentkamp