chore(test/toAdditive): remove commented test (#9971)

Co-authored-by: Moritz Firsching <[email protected]>
leanprover-community · Jan 25, 2024 · 0c4ffb6 · 0c4ffb6
1 parent b3052ec
commit 0c4ffb6
Showing 1 changed file with 0 additions and 5 deletions.
diff --git 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