Helper functions for converting reified terms back into their denotations.

def Lean.Meta.Grind.Arith.CommRing.denoteNum {M : Type → Type} [Monad M] [MonadError M] [MonadRing M] (k : Int) : M Expr

Equations

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

def Lean.Grind.CommRing.Power.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadRing M] (pw : Power) : M Lean.Expr

Equations

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

def Lean.Grind.CommRing.Mon.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadRing M] (m : Mon) : M Lean.Expr

Equations

• Lean.Grind.CommRing.Mon.unit.denoteExpr = Lean.Meta.Grind.Arith.CommRing.denoteNum 1
• (Lean.Grind.CommRing.Mon.mult pw m_2).denoteExpr = do let __do_lift ← pw.denoteExpr Lean.Grind.CommRing.Mon.denoteExpr.go✝ m_2 __do_lift

def Lean.Grind.CommRing.Poly.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadRing M] (p : Poly) : M Lean.Expr

Equations

• (Lean.Grind.CommRing.Poly.num k).denoteExpr = Lean.Meta.Grind.Arith.CommRing.denoteNum k
• (Lean.Grind.CommRing.Poly.add k m p_2).denoteExpr = do let __do_lift ← Lean.Grind.CommRing.Poly.denoteExpr.denoteTerm✝ k m Lean.Grind.CommRing.Poly.denoteExpr.go✝ p_2 __do_lift

def Lean.Grind.CommRing.Expr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [Meta.Grind.Arith.CommRing.MonadRing M] (e : Meta.Grind.Arith.CommRing.RingExpr) : M Lean.Expr

Equations

• Lean.Grind.CommRing.Expr.denoteExpr e = Lean.Grind.CommRing.Expr.denoteExpr.go✝ e

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadRing M] (c : EqCnstr) : M Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr let __do_lift_1 ← Lean.Meta.Grind.Arith.CommRing.denoteNum 0 Lean.Meta.Grind.Arith.CommRing.mkEq✝ __do_lift __do_lift_1

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadRing M] (d : PolyDerivation) : M Expr

Equations

• d.denoteExpr = d.p.denoteExpr

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadRing M] (c : DiseqCnstr) : M Expr

Equations

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

def Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr (e : Meta.Grind.Arith.CommRing.SemiringExpr) : Meta.Grind.Arith.CommRing.SemiringM Lean.Expr

Equations

• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr e = do let __do_lift ← Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr.go✝ e liftM (Lean.Meta.Grind.shareCommon __do_lift)