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

def Nat.Linear.Expr.applyPerm.go (perm : Lean.Perm) : Expr → Expr

Equations

• Nat.Linear.Expr.applyPerm.go perm (Nat.Linear.Expr.num v) = Nat.Linear.Expr.num v
• Nat.Linear.Expr.applyPerm.go perm (Nat.Linear.Expr.var i) = Nat.Linear.Expr.var (perm[i]?.getD i)
• Nat.Linear.Expr.applyPerm.go perm (a.add b) = (Nat.Linear.Expr.applyPerm.go perm a).add (Nat.Linear.Expr.applyPerm.go perm b)
• Nat.Linear.Expr.applyPerm.go perm (Nat.Linear.Expr.mulL k a) = Nat.Linear.Expr.mulL k (Nat.Linear.Expr.applyPerm.go perm a)
• Nat.Linear.Expr.applyPerm.go perm (a.mulR k) = (Nat.Linear.Expr.applyPerm.go perm a).mulR k

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 }

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.reprExpr✝ }

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.reprExprCnstr✝ }

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.reprPolyCnstr✝ }

@[reducible, inline]

abbrev Lean.Meta.Simp.Arith.Nat.LinearExpr : Type

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Simp.Arith.Nat.LinearCnstr : Type

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Simp.Arith.Nat.PolyExpr : Type

Equations

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

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)

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 }

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)

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 }

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

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.

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

• varMap : KExprMap Nat
• vars : Array Expr

@[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

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.

partial def Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr (e : Expr) : M LinearExpr

partial def Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr.visit (e : Expr) : M LinearExpr

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.

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

Equations

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

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.

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.

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

Equations

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