Skip to content

Commit cd38c4b

Browse files
committed
Remove redundant lemma
1 parent 418be3b commit cd38c4b

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

HumanEvalLean/HumanEval155.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ section Batteries
44
@[simp] theorem Nat.isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) := sorry
55
theorem Nat.mem_toDigits_base_10_isDigit (h : c ∈ toDigits 10 n) : c.isDigit := sorry
66
theorem Nat.toDigits_10_of_lt_10 (h : n < 10) : toDigits 10 n = [n.digitChar] := sorry
7-
@[simp] theorem Nat.toDigits_10_natAbs_ofNat (n : Nat) : toDigits 10 (n : Int).natAbs = toDigits 10 n := sorry
87

98
theorem Nat.toDigits_10_decompose (h : d < 10) (n : Nat) :
109
toDigits 10 (10 * n + d) = (toDigits 10 n) ++ (toDigits 10 d) :=

0 commit comments

Comments
 (0)