`ToExpr` instances for `CommRing.Poly` types.

source
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)

Instances For

source
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 }

source
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)

Instances For

source
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 }

source
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)

Instances For

source
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 }

source
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.intCast k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.intCast) (Lean.toExpr k)
- Lean.Meta.Grind.Arith.CommRing.ofRingExpr (Lean.Grind.CommRing.Expr.natCast k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.natCast) (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)

Instances For

source
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 }