Helper functions for converting reified terms back into their denotations.

def Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : Meta.Grind.Arith.CommRing.RingM Lean.Expr

Equations

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

def Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : Meta.Grind.Arith.CommRing.RingM 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.Mon.denoteExpr.go (m : Mon) (acc : Lean.Expr) : Meta.Grind.Arith.CommRing.RingM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.denoteExpr.go Lean.Grind.CommRing.Mon.unit acc = pure acc

def Lean.Grind.CommRing.Poly.denoteExpr (p : Poly) : Meta.Grind.Arith.CommRing.RingM 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.Poly.denoteExpr.denoteTerm (k : Int) (m : Mon) : Meta.Grind.Arith.CommRing.RingM Lean.Expr

Equations

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

def Lean.Grind.CommRing.Poly.denoteExpr.go (p : Poly) (acc : Lean.Expr) : Meta.Grind.Arith.CommRing.RingM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.denoteExpr.go (Lean.Grind.CommRing.Poly.num 0) acc = pure acc

def Lean.Grind.CommRing.Expr.denoteExpr (e : Meta.Grind.Arith.CommRing.RingExpr) : Meta.Grind.Arith.CommRing.RingM Lean.Expr

Equations

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

def Lean.Grind.CommRing.Expr.denoteExpr.go : Meta.Grind.Arith.CommRing.RingExpr → Meta.Grind.Arith.CommRing.RingM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Expr.denoteExpr.go (Lean.Grind.CommRing.Expr.num k) = Lean.Meta.Grind.Arith.CommRing.denoteNum✝ k
• Lean.Grind.CommRing.Expr.denoteExpr.go (Lean.Grind.CommRing.Expr.var x_1) = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure __do_lift.vars[x_1]!

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.denoteExpr (c : EqCnstr) : RingM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.denoteExpr (d : PolyDerivation) : RingM Expr

Equations

• d.denoteExpr = d.p.denoteExpr

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.denoteExpr (c : DiseqCnstr) : RingM Expr

Equations

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