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

Converts the linear polynomial into the "simplified" expression

Equations

• p.toExpr = Int.Linear.Poly.toExpr.go none p

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

Equations

• Int.Linear.Poly.toExpr.go none (Int.Linear.Poly.num k) = Int.Linear.Expr.num k
• Int.Linear.Poly.toExpr.go (some e) (Int.Linear.Poly.num 0) = e
• Int.Linear.Poly.toExpr.go (some e) (Int.Linear.Poly.num k) = e.add (Int.Linear.Expr.num k)
• Int.Linear.Poly.toExpr.go none (Int.Linear.Poly.add 1 x_2 p) = Int.Linear.Poly.toExpr.go (some (Int.Linear.Expr.var x_2)) p
• Int.Linear.Poly.toExpr.go none (Int.Linear.Poly.add k x_2 p) = Int.Linear.Poly.toExpr.go (some (Int.Linear.Expr.mulL k (Int.Linear.Expr.var x_2))) p
• Int.Linear.Poly.toExpr.go (some e) (Int.Linear.Poly.add 1 x_2 p) = Int.Linear.Poly.toExpr.go (some (e.add (Int.Linear.Expr.var x_2))) p
• Int.Linear.Poly.toExpr.go (some e) (Int.Linear.Poly.add k x_2 p) = Int.Linear.Poly.toExpr.go (some (e.add (Int.Linear.Expr.mulL k (Int.Linear.Expr.var x_2)))) p

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

Applies the given variable permutation to e

Equations

• Int.Linear.Expr.applyPerm perm e = Int.Linear.Expr.applyPerm.go perm e

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

Equations

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

instance Int.Linear.instReprPoly_lean : Repr Poly

Equations

• Int.Linear.instReprPoly_lean = { reprPrec := Int.Linear.reprPoly✝ }

instance Int.Linear.instReprExpr_lean : Repr Expr

Equations

• Int.Linear.instReprExpr_lean = { reprPrec := Int.Linear.reprExpr✝ }

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

Equations

• Lean.Meta.Simp.Arith.Int.ofPoly (Int.Linear.Poly.num a) = Lean.mkApp (Lean.mkConst `Int.Linear.Poly.num) (Lean.toExpr a)
• Lean.Meta.Simp.Arith.Int.ofPoly (Int.Linear.Poly.add a a_1 a_2) = Lean.mkApp3 (Lean.mkConst `Int.Linear.Poly.add) (Lean.toExpr a) (Lean.toExpr a_1) (Lean.Meta.Simp.Arith.Int.ofPoly a_2)

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

Equations

• Lean.Meta.Simp.Arith.Int.instToExprPoly = { toExpr := fun (a : Int.Linear.Poly) => Lean.Meta.Simp.Arith.Int.ofPoly a, toTypeExpr := Lean.mkConst `Int.Linear.Poly }

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

Equations

• Lean.Meta.Simp.Arith.Int.ofLinearExpr (Int.Linear.Expr.num v) = Lean.mkApp (Lean.mkConst `Int.Linear.Expr.num) (Lean.toExpr v)
• Lean.Meta.Simp.Arith.Int.ofLinearExpr (Int.Linear.Expr.var i) = Lean.mkApp (Lean.mkConst `Int.Linear.Expr.var) (Lean.mkNatLit i)
• Lean.Meta.Simp.Arith.Int.ofLinearExpr a.neg = Lean.mkApp (Lean.mkConst `Int.Linear.Expr.neg) (Lean.Meta.Simp.Arith.Int.ofLinearExpr a)
• Lean.Meta.Simp.Arith.Int.ofLinearExpr (a.add b) = Lean.mkApp2 (Lean.mkConst `Int.Linear.Expr.add) (Lean.Meta.Simp.Arith.Int.ofLinearExpr a) (Lean.Meta.Simp.Arith.Int.ofLinearExpr b)
• Lean.Meta.Simp.Arith.Int.ofLinearExpr (a.sub b) = Lean.mkApp2 (Lean.mkConst `Int.Linear.Expr.sub) (Lean.Meta.Simp.Arith.Int.ofLinearExpr a) (Lean.Meta.Simp.Arith.Int.ofLinearExpr b)
• Lean.Meta.Simp.Arith.Int.ofLinearExpr (Int.Linear.Expr.mulL k a) = Lean.mkApp2 (Lean.mkConst `Int.Linear.Expr.mulL) (Lean.toExpr k) (Lean.Meta.Simp.Arith.Int.ofLinearExpr a)
• Lean.Meta.Simp.Arith.Int.ofLinearExpr (a.mulR k) = Lean.mkApp2 (Lean.mkConst `Int.Linear.Expr.mulR) (Lean.Meta.Simp.Arith.Int.ofLinearExpr a) (Lean.toExpr k)

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

Equations

• Lean.Meta.Simp.Arith.Int.instToExprExpr = { toExpr := fun (a : Int.Linear.Expr) => Lean.Meta.Simp.Arith.Int.ofLinearExpr a, toTypeExpr := Lean.mkConst `Int.Linear.Expr }

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

Equations

• Int.Linear.Expr.denoteExpr ctx (Int.Linear.Expr.num v) = pure (Lean.toExpr v)
• Int.Linear.Expr.denoteExpr ctx (Int.Linear.Expr.var i) = pure (ctx i)
• Int.Linear.Expr.denoteExpr ctx a.neg = do let __do_lift ← Int.Linear.Expr.denoteExpr ctx a pure (Lean.mkIntNeg __do_lift)
• Int.Linear.Expr.denoteExpr ctx (a.add b) = do let __do_lift ← Int.Linear.Expr.denoteExpr ctx a let __do_lift_1 ← Int.Linear.Expr.denoteExpr ctx b pure (Lean.mkIntAdd __do_lift __do_lift_1)
• Int.Linear.Expr.denoteExpr ctx (a.sub b) = do let __do_lift ← Int.Linear.Expr.denoteExpr ctx a let __do_lift_1 ← Int.Linear.Expr.denoteExpr ctx b pure (Lean.mkIntSub __do_lift __do_lift_1)
• Int.Linear.Expr.denoteExpr ctx (Int.Linear.Expr.mulL k a) = do let __do_lift ← Int.Linear.Expr.denoteExpr ctx a pure (Lean.mkIntMul (Lean.toExpr k) __do_lift)
• Int.Linear.Expr.denoteExpr ctx (a.mulR k) = do let __do_lift ← Int.Linear.Expr.denoteExpr ctx a pure (Lean.mkIntMul __do_lift (Lean.toExpr k))

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

Equations

• Int.Linear.Poly.denoteExpr ctx (Int.Linear.Poly.num k) = pure (Lean.toExpr k)
• Int.Linear.Poly.denoteExpr ctx (Int.Linear.Poly.add 1 x p_2) = Int.Linear.Poly.denoteExpr.go ctx (ctx x) p_2
• Int.Linear.Poly.denoteExpr ctx (Int.Linear.Poly.add k x p_2) = Int.Linear.Poly.denoteExpr.go ctx (Lean.mkIntMul (Lean.toExpr k) (ctx x)) p_2

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

Equations

• Int.Linear.Poly.denoteExpr.go ctx r (Int.Linear.Poly.num 0) = pure r
• Int.Linear.Poly.denoteExpr.go ctx r (Int.Linear.Poly.num k) = pure (Lean.mkIntAdd r (Lean.toExpr k))
• Int.Linear.Poly.denoteExpr.go ctx r (Int.Linear.Poly.add 1 x p_2) = Int.Linear.Poly.denoteExpr.go ctx (Lean.mkIntAdd r (ctx x)) p_2
• Int.Linear.Poly.denoteExpr.go ctx r (Int.Linear.Poly.add k x p_2) = Int.Linear.Poly.denoteExpr.go ctx (Lean.mkIntAdd r (Lean.mkIntMul (Lean.toExpr k) (ctx x))) p_2

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

Equations

• Lean.Meta.Simp.Arith.Int.ToLinear.M = StateRefT' IO.RealWorld Lean.Meta.Simp.Arith.Int.ToLinear.State Lean.MetaM

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Simp.Arith.Int.eqCnstr? e = Lean.Meta.Simp.Arith.Int.adapter✝ e Lean.Meta.Simp.Arith.Int.ToLinear.eqCnstr?

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

Equations

• Lean.Meta.Simp.Arith.Int.leCnstr? e = Lean.Meta.Simp.Arith.Int.adapter✝ e Lean.Meta.Simp.Arith.Int.ToLinear.leCnstr?

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

Equations

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

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

Equations

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