theorem_proving_in_lean4 icon indicating copy to clipboard operation
theorem_proving_in_lean4 copied to clipboard
verified publisher icon leanprover

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

Open avigad opened this issue 1 year ago • 0 comments

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.

avigad avatar Jun 23 '24 20:06 avigad