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.
Instances For
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.
Instances For
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
Instances For
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
Instances For
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 using an explicit variable array.
Equations
- Lean.Meta.Sym.Arith.denoteRingExpr vars e = Lean.Meta.Sym.Arith.denoteRingExprCore✝ (fun (x : Nat) => vars[x]!) e