source
def Lean.Meta.Grind.Arith.expandPowAdd :
Simp.Simproc

Applies `a^(m+n) = a^m * a^n`, `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 comm ring module.

Equations

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

Instances For

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

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

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.

source
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.

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

Add additional arithmetic simprocs

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

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

Instances For