Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.num v) = Lean.mkApp (Lean.mkConst `Nat.Linear.Expr.num) (Lean.mkNatLit v)
- Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.var i) = Lean.mkApp (Lean.mkConst `Nat.Linear.Expr.var) (Lean.mkNatLit i)
- Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.mulL k a) = Lean.mkApp2 (Lean.mkConst `Nat.Linear.Expr.mulL) (Lean.mkNatLit k) (Lean.Meta.Linear.Nat.LinearExpr.toExpr a)
- Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.mulR a k) = Lean.mkApp2 (Lean.mkConst `Nat.Linear.Expr.mulR) (Lean.Meta.Linear.Nat.LinearExpr.toExpr a) (Lean.mkNatLit k)
Instances For
Instances For
def
Lean.Meta.Linear.Nat.LinearExpr.toArith
(ctx : Array Lean.Expr)
(e : Lean.Meta.Linear.Nat.LinearExpr)
:
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.num v) = pure (Lean.mkNatLit v)
- Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.var i) = pure ctx[i]!
- Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.mulL k a) = do let __do_lift ← Lean.Meta.Linear.Nat.LinearExpr.toArith ctx a Lean.Meta.mkMul (Lean.mkNatLit k) __do_lift
- Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.mulR a k) = do let __do_lift ← Lean.Meta.Linear.Nat.LinearExpr.toArith ctx a Lean.Meta.mkMul __do_lift (Lean.mkNatLit k)
Instances For
def
Lean.Meta.Linear.Nat.LinearCnstr.toArith
(ctx : Array Lean.Expr)
(c : Lean.Meta.Linear.Nat.LinearCnstr)
:
Instances For
- varMap : Lean.Meta.KExprMap Nat
Instances For
def
Lean.Meta.Linear.Nat.ToLinear.run
{α : Type}
(x : Lean.Meta.Linear.Nat.ToLinear.M α)
:
Lean.MetaM (α × Array Lean.Expr)