`ToExpr` instances for `Linarith.Poly` types.

source
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

Instances For

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

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

Instances For

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