source
def Nat.Linear.Expr.applyPerm (perm : Lean.Perm) (e : Expr) :
Expr

Applies the given variable permutation to `e`

Equations

- Nat.Linear.Expr.applyPerm perm e = Nat.Linear.Expr.applyPerm.go✝ perm e

Instances For

source
def Nat.Linear.ExprCnstr.applyPerm (perm : Lean.Perm) :
ExprCnstr → ExprCnstr

Applies the given variable permutation to the given expression constraint.

Equations

- Nat.Linear.ExprCnstr.applyPerm perm { eq := eq, lhs := lhs, rhs := rhs } = { eq := eq, lhs := Nat.Linear.Expr.applyPerm perm lhs, rhs := Nat.Linear.Expr.applyPerm perm rhs }

Instances For

source
instance Lean.Meta.Simp.Arith.Nat.instReprExpr_lean :
Repr Nat.Linear.Expr
Equations

- Lean.Meta.Simp.Arith.Nat.instReprExpr_lean = { reprPrec := Lean.Meta.Simp.Arith.Nat.instReprExpr_lean.repr }

source
def Lean.Meta.Simp.Arith.Nat.instReprExpr_lean.repr :
Nat.Linear.Expr → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean.repr :
Nat.Linear.ExprCnstr → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean :
Repr Nat.Linear.ExprCnstr
Equations

- Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean = { reprPrec := Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean.repr }

source
instance Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean :
Repr Nat.Linear.PolyCnstr
Equations

- Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean = { reprPrec := Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean.repr }

source
def Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean.repr :
Nat.Linear.PolyCnstr → Nat → Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.Arith.Nat.LinearExpr :
Type
Equations

- Lean.Meta.Simp.Arith.Nat.LinearExpr = Nat.Linear.Expr

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.Arith.Nat.LinearCnstr :
Type
Equations

- Lean.Meta.Simp.Arith.Nat.LinearCnstr = Nat.Linear.ExprCnstr

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.Arith.Nat.PolyExpr :
Type
Equations

- Lean.Meta.Simp.Arith.Nat.PolyExpr = Nat.Linear.Poly

Instances For

source
def Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr (e : LinearExpr) :
Expr
Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr (Nat.Linear.Expr.num v) = Lean.mkApp (Lean.mkConst `Nat.Linear.Expr.num) (Lean.mkNatLit v)
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr (Nat.Linear.Expr.var i) = Lean.mkApp (Lean.mkConst `Nat.Linear.Expr.var) (Lean.mkNatLit i)
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr (Nat.Linear.Expr.mulL k a) = Lean.mkApp2 (Lean.mkConst `Nat.Linear.Expr.mulL) (Lean.mkNatLit k) (Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr a)
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr (a.mulR k) = Lean.mkApp2 (Lean.mkConst `Nat.Linear.Expr.mulR) (Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr a) (Lean.mkNatLit k)

Instances For

source
instance Lean.Meta.Simp.Arith.Nat.instToExprLinearExpr :
ToExpr LinearExpr
Equations

- Lean.Meta.Simp.Arith.Nat.instToExprLinearExpr = { toExpr := fun (a : Lean.Meta.Simp.Arith.Nat.LinearExpr) => a.toExpr, toTypeExpr := Lean.mkConst `Nat.Linear.Expr }

source
def Lean.Meta.Simp.Arith.Nat.LinearCnstr.toExpr (c : LinearCnstr) :
Expr
Equations

- c.toExpr = Lean.mkApp3 (Lean.mkConst `Nat.Linear.ExprCnstr.mk) (Lean.toExpr c.eq) (Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr c.lhs) (Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr c.rhs)

Instances For

source
instance Lean.Meta.Simp.Arith.Nat.instToExprLinearCnstr :
ToExpr LinearCnstr
Equations

- Lean.Meta.Simp.Arith.Nat.instToExprLinearCnstr = { toExpr := fun (a : Lean.Meta.Simp.Arith.Nat.LinearCnstr) => a.toExpr, toTypeExpr := Lean.mkConst `Nat.Linear.ExprCnstr }

source
def Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) :
MetaM Expr
Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.num v) = pure (Lean.mkNatLit v)
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.var i) = pure ctx[i]!
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.mulL k a) = do let __do_lift ← Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith ctx a pure (Lean.mkNatMul (Lean.mkNatLit k) __do_lift)
- Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith ctx (a.mulR k) = do let __do_lift ← Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith ctx a pure (Lean.mkNatMul __do_lift (Lean.mkNatLit k))

Instances For

source
def Lean.Meta.Simp.Arith.Nat.LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) :
MetaM Expr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Lean.Meta.Simp.Arith.Nat.ToLinear.State :
Type

- varMap : KExprMap Nat
- vars : Array Expr

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.Arith.Nat.ToLinear.M (α : Type) :
Type
Equations

- Lean.Meta.Simp.Arith.Nat.ToLinear.M = StateRefT' IO.RealWorld Lean.Meta.Simp.Arith.Nat.ToLinear.State Lean.MetaM

Instances For

source
def Lean.Meta.Simp.Arith.Nat.ToLinear.addAsVar (e : Expr) :
M LinearExpr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr (e : Expr) :
M LinearExpr
source
def Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearCnstr? (e : Expr) :
M (Option LinearCnstr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Simp.Arith.Nat.ToLinear.run {α : Type} (x : M α) :
MetaM (α × Array Expr)
Equations

- Lean.Meta.Simp.Arith.Nat.ToLinear.run x = do let __discr ← StateRefT'.run x { } match __discr with | (a, s) => pure (a, s.vars)

Instances For

source
def Lean.Meta.Simp.Arith.Nat.toLinearExpr (e : Expr) :
MetaM (LinearExpr × Array Expr)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Simp.Arith.Nat.toLinearCnstr? (e : Expr) :
MetaM (Option (LinearCnstr × Array Expr))
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Simp.Arith.Nat.toContextExpr (ctx : Array Expr) :
MetaM Expr
Equations

- One or more equations did not get rendered due to their size.

Instances For