Cached function expressions for arithmetic operators

Synthesizes and caches the canonical Lean expressions for arithmetic operators (+, *, -, ^, intCast, natCast, etc.). These cached expressions are used during reification to validate instances via pointer equality (isSameExpr).

Each getter checks the cache field first. On a miss, it synthesizes the instance, verifies it against the expected instance from the ring structure using isDefEqI, canonicalizes the result via canonExpr, and stores it.

def Lean.Meta.Sym.Arith.getNatSMulFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getIntSMulFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getAddFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getMulFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getSubFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getNegFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getIntCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getInvFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getDivFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getNatSMulFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getAddFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getMulFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getPowFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getNatCastFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Sym.Arith.getToQFn {m : Type → Type} [Monad m] [MonadCanon m] [MonadCommSemiring m] : m Expr

The embedding OfSemiring.toQ of the semiring into its envelope ring.

Equations

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

def Lean.Meta.Sym.Arith.getAddRightCancelInst? {m : Type → Type} [Monad m] [MonadCanon m] [MonadCommSemiring m] : m (Option Expr)

The AddRightCancel instance of the semiring, if any. The result of the search is cached.

Equations

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