def Lean.Meta.Grind.Arith.mkSemiringThm (declName : Name) (α : Expr) : MetaM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.expandPow01 : Simp.Simproc

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

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.expandDiv : Simp.Simproc

Equations

• One or more equations did not get rendered due to their size.

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.

def Lean.Meta.Grind.Arith.normInst (instPos : Nat) (inst e : Expr) : SimpM Simp.DStep

Generic instance normalizer

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.normNatAddInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatAddInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Nat.mkInstHAdd

def Lean.Meta.Grind.Arith.normNatMulInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatMulInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Nat.mkInstHMul

def Lean.Meta.Grind.Arith.normNatSubInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatSubInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Nat.mkInstHSub

def Lean.Meta.Grind.Arith.normNatDivInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatDivInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Nat.mkInstHDiv

def Lean.Meta.Grind.Arith.normNatModInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatModInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Nat.mkInstMod

def Lean.Meta.Grind.Arith.normNatPowInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatPowInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Nat.mkInstHPow

def Lean.Meta.Grind.Arith.normNatOfNatInst : Simp.DSimproc

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.normIntNegInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntNegInst = Lean.Meta.Grind.Arith.normInst 1 Lean.Int.mkInstNeg

def Lean.Meta.Grind.Arith.normIntAddInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntAddInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Int.mkInstHAdd

def Lean.Meta.Grind.Arith.normIntMulInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntMulInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Int.mkInstHMul

def Lean.Meta.Grind.Arith.normIntSubInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntSubInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Int.mkInstHSub

def Lean.Meta.Grind.Arith.normIntDivInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntDivInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Int.mkInstHDiv

def Lean.Meta.Grind.Arith.normIntModInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntModInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Int.mkInstMod

def Lean.Meta.Grind.Arith.normIntPowInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normIntPowInst = Lean.Meta.Grind.Arith.normInst 3 Lean.Int.mkInstHPow

def Lean.Meta.Grind.Arith.normNatCastInst : Simp.DSimproc

Equations

• Lean.Meta.Grind.Arith.normNatCastInst = Lean.Meta.Grind.Arith.normInst 1 Lean.Int.mkInstNatCast

def Lean.Meta.Grind.Arith.normIntOfNatInst : Simp.DSimproc

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.normNatCastNum : Simp.Simproc

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.normIntCastNum : Simp.Simproc

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.normPowRatInt : Simp.DSimproc

Equations

• One or more equations did not get rendered due to their size.

Add additional arithmetic simprocs

def Lean.Meta.Grind.Arith.addSimproc (s : Simprocs) : CoreM Simprocs

Equations

• One or more equations did not get rendered due to their size.