← Copula mathematical handbook

ToExpr instances for CommRing.Poly types.

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

Equations

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

@[instance_reducible]

instance Lean.Meta.Sym.Arith.instToExprPower : ToExpr Power

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.Meta.Sym.Arith.instToExprMon : ToExpr Mon

Equations

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

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

Equations

• Lean.Meta.Sym.Arith.ofPoly (Lean.Grind.CommRing.Poly.num k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Poly.num) (Lean.toExpr k)
• Lean.Meta.Sym.Arith.ofPoly (Lean.Grind.CommRing.Poly.add k m p_2) = Lean.mkApp3 (Lean.mkConst `Lean.Grind.CommRing.Poly.add) (Lean.toExpr k) (Lean.toExpr m) (Lean.Meta.Sym.Arith.ofPoly p_2)

@[instance_reducible]

instance Lean.Meta.Sym.Arith.instToExprPoly : ToExpr Poly

Equations

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

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

Equations

• Lean.Meta.Sym.Arith.ofRingExpr (Lean.Grind.CommRing.Expr.num k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.num) (Lean.toExpr k)
• Lean.Meta.Sym.Arith.ofRingExpr (Lean.Grind.CommRing.Expr.intCast k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.intCast) (Lean.toExpr k)
• Lean.Meta.Sym.Arith.ofRingExpr (Lean.Grind.CommRing.Expr.natCast k) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.natCast) (Lean.toExpr k)
• Lean.Meta.Sym.Arith.ofRingExpr (Lean.Grind.CommRing.Expr.var x) = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.var) (Lean.toExpr x)
• Lean.Meta.Sym.Arith.ofRingExpr (a.add b) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Expr.add) (Lean.Meta.Sym.Arith.ofRingExpr a) (Lean.Meta.Sym.Arith.ofRingExpr b)
• Lean.Meta.Sym.Arith.ofRingExpr (a.mul b) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Expr.mul) (Lean.Meta.Sym.Arith.ofRingExpr a) (Lean.Meta.Sym.Arith.ofRingExpr b)
• Lean.Meta.Sym.Arith.ofRingExpr (a.sub b) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Expr.sub) (Lean.Meta.Sym.Arith.ofRingExpr a) (Lean.Meta.Sym.Arith.ofRingExpr b)
• Lean.Meta.Sym.Arith.ofRingExpr a.neg = Lean.mkApp (Lean.mkConst `Lean.Grind.CommRing.Expr.neg) (Lean.Meta.Sym.Arith.ofRingExpr a)
• Lean.Meta.Sym.Arith.ofRingExpr (a.pow k) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.CommRing.Expr.pow) (Lean.Meta.Sym.Arith.ofRingExpr a) (Lean.toExpr k)

@[instance_reducible]

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

Equations

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