search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

Remove outdated syntax information #115

Open digama0 opened 2 years ago

digama0 commented 2 years ago

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

abentkamp commented 1 year ago

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