diff --git a/test/toAdditive.lean b/test/toAdditive.lean index 85aec546bd8e0..ed344ce099c1b 100644 --- a/test/toAdditive.lean +++ b/test/toAdditive.lean @@ -221,11 +221,6 @@ attribute [to_additive add_some_def] some_def run_cmd do liftCoreM <| successIfFail (getConstInfo `Test.add_some_def.in_namespace) --- [todo] currently this test breaks. --- example : (AddUnits.mk_of_add_eq_zero 0 0 (by simp) : ℕ) --- = (AddUnits.mk_of_add_eq_zero 0 0 (by simp) : ℕ) := --- by norm_cast - section set_option linter.unusedVariables false