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

Converts the linear polynomial into the "simplified" expression

def Int.Linear.Poly.toExpr.go : Option Expr → Poly → Expr

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

Applies the given variable permutation to e

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

instance Int.Linear.instReprPoly_lean : Repr Poly

instance Int.Linear.instReprExpr_lean : Repr Expr

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

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

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

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

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

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

def Int.Linear.Poly.denoteExpr.go (ctx : Nat → Lean.Expr) (r : 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.Linear.Expr

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

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

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

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

def Lean.Meta.Simp.Arith.Int.ToLinear.dvdCnstr? (e : Expr) : M (Option (Int × Int.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.Linear.Expr × Array Expr)

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

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

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

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