Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr

Helper functions for converting reified terms back into their denotations.

source
def Lean.Meta.Grind.Arith.CommRing.denoteNum {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M] (k : Int) :
M Expr
Equations
    Instances For
      source
      def Lean.Grind.CommRing.Power.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadCanon M] [Meta.Grind.Arith.CommRing.MonadRing M] (pw : Power) :
      M Lean.Expr
      Equations
        Instances For
          source
          def Lean.Grind.CommRing.Mon.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadCanon M] [Meta.Grind.Arith.CommRing.MonadRing M] (m : Mon) :
          M Lean.Expr
          Equations
            Instances For
              source
              def Lean.Grind.CommRing.Poly.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadCanon M] [Meta.Grind.Arith.CommRing.MonadRing M] (p : Poly) :
              M Lean.Expr
              Equations
                Instances For
                  source
                  def Lean.Grind.CommRing.Expr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadCanon M] [Meta.Grind.Arith.CommRing.MonadRing M] (e : Meta.Grind.Arith.CommRing.RingExpr) :
                  M Lean.Expr
                  Equations
                    Instances For
                      source
                      def Lean.Grind.CommRing.Expr.denoteExpr' {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadCanon M] [Meta.Grind.Arith.CommRing.MonadRing M] (vars : Array Lean.Expr) (e : Meta.Grind.Arith.CommRing.RingExpr) :
                      M Lean.Expr
                      Equations
                        Instances For
                          source
                          def Lean.Meta.Grind.Arith.CommRing.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M] (c : EqCnstr) :
                          M Expr
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M] (d : PolyDerivation) :
                              M Expr
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M] (c : DiseqCnstr) :
                                  M Expr
                                  Equations
                                    Instances For