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

Applies the given variable permutation to e

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

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

Applies the given variable permutation to the given expression constraint.

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

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

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

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

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

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

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

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

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

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

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

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)

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

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

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

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