def Int.Internal.Linear.Poly.toExpr (p : Poly) : Expr

Converts the linear polynomial into the "simplified" expression

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

Applies the given variable permutation to e

@[instance_reducible]

instance Int.Internal.Linear.instReprPoly_lean : Repr Poly

def Int.Internal.Linear.instReprPoly_lean.repr : Poly → Nat → Std.Format

def Int.Internal.Linear.instReprExpr_lean.repr : Expr → Nat → Std.Format

@[instance_reducible]

instance Int.Internal.Linear.instReprExpr_lean : Repr Expr

def Lean.Meta.Simp.Arith.Int.ofPoly (p : Int.Internal.Linear.Poly) : Expr

@[instance_reducible]

instance Lean.Meta.Simp.Arith.Int.instToExprPoly : ToExpr Int.Internal.Linear.Poly

def Lean.Meta.Simp.Arith.Int.ofLinearExpr (e : Int.Internal.Linear.Expr) : Expr

@[instance_reducible]

instance Lean.Meta.Simp.Arith.Int.instToExprExpr : ToExpr Int.Internal.Linear.Expr

def Int.Internal.Linear.Expr.denoteExpr (ctx : Nat → Lean.Expr) (e : Expr) : Lean.MetaM Lean.Expr

def Int.Internal.Linear.Poly.denoteExpr (ctx : Nat → Lean.Expr) (p : Poly) : Lean.MetaM Lean.Expr

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

• varMap : KExprMap Nat
• vars : Array Expr

@[reducible, inline]

abbrev Lean.Meta.Simp.Arith.Int.ToLinear.M (α : Type) : Type

def Lean.Meta.Simp.Arith.Int.ToLinear.addAsVar (e : Expr) : M Int.Internal.Linear.Expr

partial def Lean.Meta.Simp.Arith.Int.ToLinear.toLinearExpr (e : Expr) : M Int.Internal.Linear.Expr

def Lean.Meta.Simp.Arith.Int.ToLinear.eqCnstr? (e : Expr) : M (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr))

def Lean.Meta.Simp.Arith.Int.ToLinear.leCnstr? (e : Expr) : M (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr))

def Lean.Meta.Simp.Arith.Int.ToLinear.dvdCnstr? (e : Expr) : M (Option (Int × Int.Internal.Linear.Expr))

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

def Lean.Meta.Simp.Arith.Int.toLinearExpr (e : Expr) : MetaM (Int.Internal.Linear.Expr × Array Expr)

def Lean.Meta.Simp.Arith.Int.eqCnstr? (e : Expr) : MetaM (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr × Array Expr))

def Lean.Meta.Simp.Arith.Int.leCnstr? (e : Expr) : MetaM (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr × Array Expr))

def Lean.Meta.Simp.Arith.Int.dvdCnstr? (e : Expr) : MetaM (Option (Int × Int.Internal.Linear.Expr × Array Expr))

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