Skip to content

Commit 2a80c53

Browse files
committed
Remove redundant lemma
1 parent a30a5f1 commit 2a80c53

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

HumanEvalLean/HumanEval155.lean

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
1-
-- TODO: This already exists in Mathlib.
2-
@[simp] theorem Nat.natAbs_cast (n : Nat) : (n : Int).natAbs = n := rfl
3-
41
section Batteries
52

63
-- https://github.com/leanprover-community/batteries/pull/1267

0 commit comments

Comments
 (0)