Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr

Helper functions for converting reified terms back into their denotations.

source
def Lean.Grind.Linarith.Poly.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.Linear.MonadGetStruct M] (p : Poly) :
M Lean.Expr
Equations
    Instances For
      source
      def Lean.Grind.Linarith.Poly.denoteExpr.denoteTerm {M : Type → Type} [Monad M] [Meta.Grind.Arith.Linear.MonadGetStruct M] (k : Int) (x : Var) :
      M Lean.Expr
      Equations
        Instances For
          source
          def Lean.Grind.Linarith.Poly.denoteExpr.go {M : Type → Type} [Monad M] [Meta.Grind.Arith.Linear.MonadGetStruct M] (p : Poly) (acc : Lean.Expr) :
          M Lean.Expr
          Equations
            Instances For
              source
              def Lean.Grind.Linarith.Expr.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.Linear.MonadGetStruct M] (e : Meta.Grind.Arith.Linear.LinExpr) :
              M Lean.Expr
              Equations
                Instances For
                  source
                  def Lean.Grind.Linarith.Expr.denoteExpr.go {M : Type → Type} [Monad M] [Meta.Grind.Arith.Linear.MonadGetStruct M] :
                  Meta.Grind.Arith.Linear.LinExpr → M Lean.Expr
                  Equations
                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : DiseqCnstr) :
                      M Expr
                      Equations
                        Instances For
                          source
                          def Lean.Meta.Grind.Arith.Linear.IneqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] [MonadError M] (c : IneqCnstr) :
                          M Expr
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.Linear.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : EqCnstr) :
                              M Expr
                              Equations
                                Instances For
                                  source
                                  def Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Poly) :
                                  Meta.Grind.Arith.Linear.LinearM Lean.Expr
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Poly) (generation : Nat := 0) :
                                      Meta.Grind.Arith.Linear.LinearM Lean.Expr
                                      Equations
                                        Instances For