Denotation of reified expressions

Converts reified RingExpr, Poly, Mon, Power back into Lean Exprs using the ring's cached operator functions and variable array.

def Lean.Meta.Sym.Arith.denoteNum {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] (k : Int) : m Expr

Convert an integer to a numeral expression in the ring. Negative values use getNegFn.

Equations

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

def Lean.Meta.Sym.Arith.denotePower {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] [MonadGetVar m] (pw : Power) : m Expr

Denote a Power (variable raised to a power).

Equations

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

def Lean.Meta.Sym.Arith.denoteMon {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] [MonadGetVar m] (mn : Mon) : m Expr

Denote a Mon (product of powers).

Equations

• Lean.Meta.Sym.Arith.denoteMon Lean.Grind.CommRing.Mon.unit = Lean.Meta.Sym.Arith.denoteNum 1
• Lean.Meta.Sym.Arith.denoteMon (Lean.Grind.CommRing.Mon.mult pw mn_2) = do let __do_lift ← Lean.Meta.Sym.Arith.denotePower pw Lean.Meta.Sym.Arith.denoteMon.go✝ mn_2 __do_lift

def Lean.Meta.Sym.Arith.denotePoly {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] [MonadGetVar m] (p : Poly) : m Expr

Denote a Poly (sum of coefficient × monomial terms).

Equations

• Lean.Meta.Sym.Arith.denotePoly (Lean.Grind.CommRing.Poly.num k) = Lean.Meta.Sym.Arith.denoteNum k
• Lean.Meta.Sym.Arith.denotePoly (Lean.Grind.CommRing.Poly.add k mn p_2) = do let __do_lift ← Lean.Meta.Sym.Arith.denotePoly.denoteTerm✝ k mn Lean.Meta.Sym.Arith.denotePoly.go✝ p_2 __do_lift

def Lean.Meta.Sym.Arith.denoteRingExpr {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] [MonadGetVar m] (e : RingExpr) : m Expr

Denote a RingExpr whose variables are the current ring's, looked up with getVar.

Equations

• Lean.Meta.Sym.Arith.denoteRingExpr e = Lean.Meta.Sym.Arith.denoteRingExprCore✝ Lean.Meta.Sym.Arith.getVar e

def Lean.Meta.Sym.Arith.denoteRingExpr' {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] (vars : Array Expr) (e : RingExpr) : m Expr

Denote a RingExpr whose variables index vars instead of the current ring's variables. Proof terms rename the variables of an expression to the compact range 0 .. n-1 of the variables it actually uses (see renameVars), and build an RArray context out of those n terms; the denotation of the renamed expression must use that same array.

Equations

• Lean.Meta.Sym.Arith.denoteRingExpr' vars e = Lean.Meta.Sym.Arith.denoteRingExprCore✝ (fun (x : Nat) => pure vars[x]!) e

def Lean.Meta.Sym.Arith.denoteNatNum {m : Type → Type} [Monad m] [MonadCanon m] [MonadSemiring m] (k : Nat) : m Expr

Convert a natural number to a numeral expression in the semiring.

Equations

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

def Lean.Meta.Sym.Arith.denoteSemiringExpr' {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadSemiring m] (vars : Array Expr) (e : SemiringExpr) : m Expr

Denote a SemiringExpr whose variables index vars, using the semiring's operators. Fails on the constructors that have no semiring denotation (sub, neg, intCast, negative numerals).

Equations

• Lean.Meta.Sym.Arith.denoteSemiringExpr' vars e = Lean.Meta.Sym.Arith.denoteSemiringExpr'.go✝ vars e