ToExpr instances for CommRing.Poly types.

def Lean.Meta.Grind.Arith.CommRing.ofPower (p : Power) : Expr

Equations

• Lean.Meta.Grind.Arith.CommRing.ofPower p = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Power.mk) (Lean.toExpr p.x) (Lean.toExpr p.k)

instance Lean.Meta.Grind.Arith.CommRing.instToExprPower : ToExpr Power

Equations

• Lean.Meta.Grind.Arith.CommRing.instToExprPower = { toExpr := Lean.Meta.Grind.Arith.CommRing.ofPower, toTypeExpr := Lean.mkConst `Lean.Grind.CommRing.Power }

def Lean.Meta.Grind.Arith.CommRing.ofMon (m : Mon) : Expr

Equations

• Lean.Meta.Grind.Arith.CommRing.ofMon Lean.Grind.CommRing.Mon.unit = Lean.mkConst `Lean.Grind.CommRing.Mon.unit
• Lean.Meta.Grind.Arith.CommRing.ofMon (Lean.Grind.CommRing.Mon.mult pw m_2) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Mon.mult) (Lean.toExpr pw) (Lean.Meta.Grind.Arith.CommRing.ofMon m_2)

instance Lean.Meta.Grind.Arith.CommRing.instToExprMon : ToExpr Mon

Equations

• Lean.Meta.Grind.Arith.CommRing.instToExprMon = { toExpr := Lean.Meta.Grind.Arith.CommRing.ofMon, toTypeExpr := Lean.mkConst `Lean.Grind.CommRing.Mon }

def Lean.Meta.Grind.Arith.CommRing.ofPoly (p : Poly) : Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.CommRing.ofPoly (Lean.Grind.CommRing.Poly.num k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Poly.num) (Lean.toExpr k)

instance Lean.Meta.Grind.Arith.CommRing.instToExprPoly : ToExpr Poly

Equations

• Lean.Meta.Grind.Arith.CommRing.instToExprPoly = { toExpr := Lean.Meta.Grind.Arith.CommRing.ofPoly, toTypeExpr := Lean.mkConst `Lean.Grind.CommRing.Poly }

def Lean.Meta.Grind.Arith.CommRing.ofRingExpr (e : Grind.CommRing.Expr) : Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.CommRing.ofRingExpr (Lean.Grind.CommRing.Expr.num k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.num) (Lean.toExpr k)
• Lean.Meta.Grind.Arith.CommRing.ofRingExpr (Lean.Grind.CommRing.Expr.var x) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.var) (Lean.toExpr x)
• Lean.Meta.Grind.Arith.CommRing.ofRingExpr a.neg = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.neg) (Lean.Meta.Grind.Arith.CommRing.ofRingExpr a)
• Lean.Meta.Grind.Arith.CommRing.ofRingExpr (a.pow k) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Expr.pow) (Lean.Meta.Grind.Arith.CommRing.ofRingExpr a) (Lean.toExpr k)

instance Lean.Meta.Grind.Arith.CommRing.instToExprExpr : ToExpr Grind.CommRing.Expr

Equations

• Lean.Meta.Grind.Arith.CommRing.instToExprExpr = { toExpr := Lean.Meta.Grind.Arith.CommRing.ofRingExpr, toTypeExpr := Lean.mkConst `Lean.Grind.CommRing.Expr }

def Lean.Meta.Grind.Arith.CommRing.ofNullCert (nc : Grind.CommRing.NullCert) : Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.CommRing.ofNullCert Lean.Grind.CommRing.NullCert.empty = Lean.mkConst `Lean.Grind.CommRing.NullCert.empty

instance Lean.Meta.Grind.Arith.CommRing.instToExprNullCert : ToExpr Grind.CommRing.NullCert

Equations

• Lean.Meta.Grind.Arith.CommRing.instToExprNullCert = { toExpr := Lean.Meta.Grind.Arith.CommRing.ofNullCert, toTypeExpr := Lean.mkConst `Lean.Grind.CommRing.NullCert }