Examples in Inductive Types chapter broken due to `simp_eq_add_one` simp rule - Githubissues

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4

https://leanprover.github.io/theorem_proving_in_lean4/

Apache License 2.0

159 stars 85 forks source link

Examples in Inductive Types chapter broken due to `simp_eq_add_one` simp rule #120

Open avigad opened 3 months ago

avigad commented 3 months ago

As noted on Zulip, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/experiment.20making.20.60succ_eq_add_one.60.20.40.5Bsimp.5D.60/near/446392853.