Helper functions for converting reified terms back into their denotations.

def Lean.Grind.Linarith.Poly.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.Arith.Linear.MonadGetStruct M] (p : Poly) : M Lean.Expr

Equations

• Lean.Grind.Linarith.Poly.nil.denoteExpr = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.zero
• (Lean.Grind.Linarith.Poly.add k m p_2).denoteExpr = do let __do_lift ← Lean.Grind.Linarith.Poly.denoteExpr.denoteTerm k m Lean.Grind.Linarith.Poly.denoteExpr.go p_2 __do_lift

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.
• Lean.Grind.Linarith.Poly.denoteExpr.go Lean.Grind.Linarith.Poly.nil acc = pure acc

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

• Lean.Grind.Linarith.Expr.denoteExpr e = Lean.Grind.Linarith.Expr.denoteExpr.go e

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

• One or more equations did not get rendered due to their size.
• Lean.Grind.Linarith.Expr.denoteExpr.go Lean.Grind.Linarith.Expr.zero = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.zero
• Lean.Grind.Linarith.Expr.denoteExpr.go (Lean.Grind.Linarith.Expr.var x_1) = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct pure __do_lift.vars[x_1]!

def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : DiseqCnstr) : M Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Linear.IneqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] [MonadError M] (c : IneqCnstr) : M Expr

Equations

• c.denoteExpr = Lean.Meta.Grind.Arith.Linear.denoteIneq✝ c.p c.strict

def Lean.Meta.Grind.Arith.Linear.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : EqCnstr) : M Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr let __do_lift_1 ← Lean.Meta.Grind.Arith.Linear.getStruct Lean.Meta.Grind.Arith.Linear.mkEq✝ __do_lift __do_lift_1.ofNatZero

def Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Poly) : Meta.Grind.Arith.Linear.LinearM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Grind.CommRing.Poly.num k).denoteAsIntModuleExpr = Lean.Meta.Grind.Arith.Linear.denoteNum✝ k

def Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Poly) (generation : Nat := 0) : Meta.Grind.Arith.Linear.LinearM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.