chore: missing grind normalization

This PR adds `Nat.sub_zero` as a `grind` normalization rule.
2026-03-17 18:34:06 +00:00 · 2025-09-19 11:42:18 -07:00
1 changed files with 1 additions and 1 deletions
--- 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