diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index 53a2206018..d535f1d337 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -182,7 +182,7 @@ init_grind_norm Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq Nat.div_zero Nat.mod_zero Nat.div_one Nat.mod_one Nat.sub_sub Nat.pow_zero Nat.pow_one Nat.sub_self - Nat.one_pow Nat.zero_sub + Nat.one_pow Nat.zero_sub Nat.sub_zero -- Int Int.lt_eq Int.emod_neg Int.ediv_neg