← Copula mathematical handbook

ToExpr instances for Linarith.Poly types.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.Linear.ofPoly Lean.Grind.Linarith.Poly.nil = Lean.mkConst `Lean.Grind.Linarith.Poly.nil

@[instance_reducible]

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

Equations

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

def Lean.Meta.Grind.Arith.Linear.ofLinExpr (e : Grind.Linarith.Expr) : Expr

Equations

• Lean.Meta.Grind.Arith.Linear.ofLinExpr Lean.Grind.Linarith.Expr.zero = Lean.mkConst `Lean.Grind.Linarith.Expr.zero
• Lean.Meta.Grind.Arith.Linear.ofLinExpr (Lean.Grind.Linarith.Expr.var x) = Lean.mkApp (Lean.mkConst `Lean.Grind.Linarith.Expr.var) (Lean.toExpr x)
• Lean.Meta.Grind.Arith.Linear.ofLinExpr (a.add b) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.Linarith.Expr.add) (Lean.Meta.Grind.Arith.Linear.ofLinExpr a) (Lean.Meta.Grind.Arith.Linear.ofLinExpr b)
• Lean.Meta.Grind.Arith.Linear.ofLinExpr (a.sub b) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.Linarith.Expr.sub) (Lean.Meta.Grind.Arith.Linear.ofLinExpr a) (Lean.Meta.Grind.Arith.Linear.ofLinExpr b)
• Lean.Meta.Grind.Arith.Linear.ofLinExpr a.neg = Lean.mkApp (Lean.mkConst `Lean.Grind.Linarith.Expr.neg) (Lean.Meta.Grind.Arith.Linear.ofLinExpr a)
• Lean.Meta.Grind.Arith.Linear.ofLinExpr (Lean.Grind.Linarith.Expr.natMul k a) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.Linarith.Expr.natMul) (Lean.toExpr k) (Lean.Meta.Grind.Arith.Linear.ofLinExpr a)
• Lean.Meta.Grind.Arith.Linear.ofLinExpr (Lean.Grind.Linarith.Expr.intMul k a) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.Linarith.Expr.intMul) (Lean.toExpr k) (Lean.Meta.Grind.Arith.Linear.ofLinExpr a)

@[instance_reducible]

instance Lean.Meta.Grind.Arith.Linear.instToExprExpr : ToExpr Grind.Linarith.Expr

Equations

• Lean.Meta.Grind.Arith.Linear.instToExprExpr = { toExpr := Lean.Meta.Grind.Arith.Linear.ofLinExpr, toTypeExpr := Lean.mkConst `Lean.Grind.Linarith.Expr }