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] [MonadGetVar m] (e : RingExpr) :
          m Expr

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

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

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

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

                Instances For