Documentation

Lean.Meta.Sym.Arith.DenoteExpr

Denotation of reified expressions #

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

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

Instances For
    source
    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).

    Instances For
      source
      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).

      Instances For
        source
        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).

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

          Instances For