Documentation

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

Helper functions for converting reified terms back into their denotations.

source
def Lean.Grind.CommRing.Power.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (pw : Power) :
M Lean.Expr
Equations
    Instances For
      source
      def Lean.Grind.CommRing.Mon.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (m : Mon) :
      M Lean.Expr
      Equations
        Instances For
          source
          def Lean.Grind.CommRing.Mon.denoteExpr.go {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (m : Mon) (acc : Lean.Expr) :
          M Lean.Expr
          Equations
            Instances For
              source
              def Lean.Grind.CommRing.Poly.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (p : Poly) :
              M Lean.Expr
              Equations
                Instances For
                  source
                  def Lean.Grind.CommRing.Poly.denoteExpr.denoteTerm {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (k : Int) (m : Mon) :
                  M Lean.Expr
                  Equations
                    Instances For
                      source
                      def Lean.Grind.CommRing.Poly.denoteExpr.go {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (p : Poly) (acc : Lean.Expr) :
                      M Lean.Expr
                      Equations
                        Instances For
                          source
                          def Lean.Grind.CommRing.Expr.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] (e : Meta.Grind.Arith.CommRing.RingExpr) :
                          M Lean.Expr
                          Equations
                            Instances For
                              source
                              def Lean.Grind.CommRing.Expr.denoteExpr.go {M : Type → Type} [Monad M] [Meta.Grind.Arith.CommRing.MonadGetRing M] :
                              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] [MonadGetRing M] (c : EqCnstr) :
                                  M Expr
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.denoteExpr {M : Type → Type} [Monad M] [MonadGetRing M] (d : PolyDerivation) :
                                      M Expr
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetRing M] (c : DiseqCnstr) :
                                          M Expr
                                          Equations
                                            Instances For