Applies a^0 = 1, a^1 = a.
We do normalize a^0 and a^1 when converting expressions into polynomials,
but we need to normalize them here when for other preprocessing steps such as
a / b = a*b⁻¹. If b is of the form c^1, it will be treated as an
atom in the ring module.
Note: We used to expand a^(n+m) here, but it prevented grind from solving
simple problems such as
example {k : Nat} (h : k - 1 + 1 = k) :
2 ^ (k - 1 + 1) = 2 ^ k := by
grind
We now use a propagator for a^(n+m) which adds the a^n*a^m to the equivalence class.
Equations
Instances For
Normalize arithmetic instances for Nat and Int operations.
Recall that both Nat and Int have builtin support in grind,
and we use the default instances. However, Mathlib may register
nonstandard ones after instances such as
instance instDistrib : Distrib Nat where
mul := (· * ·)
are added to the environment.
Generic instance normalizer
Equations
Instances For
Add additional arithmetic simprocs