def Int.Linear.Poly.renameVars (p : Poly) (f : Lean.Meta.Grind.VarRename) : Poly

Equations

• (Int.Linear.Poly.num k).renameVars f = Int.Linear.Poly.num k
• (Int.Linear.Poly.add k x p_2).renameVars f = Int.Linear.Poly.add k ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x) (p_2.renameVars f)

def Int.Linear.Expr.renameVars (e : Expr) (f : Lean.Meta.Grind.VarRename) : Expr

Equations

• (Int.Linear.Expr.num v).renameVars f = Int.Linear.Expr.num v
• (Int.Linear.Expr.var x).renameVars f = Int.Linear.Expr.var ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x)
• a.neg.renameVars f = (a.renameVars f).neg
• (a.add b).renameVars f = (a.renameVars f).add (b.renameVars f)
• (a.sub b).renameVars f = (a.renameVars f).sub (b.renameVars f)
• (Int.Linear.Expr.mulL k a).renameVars f = Int.Linear.Expr.mulL k (a.renameVars f)
• (a.mulR k).renameVars f = (a.renameVars f).mulR k

def Int.Linear.Poly.collectVars (p : Poly) : Lean.Meta.Grind.VarCollector

Equations

• (Int.Linear.Poly.num k).collectVars = id
• (Int.Linear.Poly.add k x p_2).collectVars = Lean.Meta.Grind.collectVar x >> p_2.collectVars

def Int.Linear.Expr.collectVars (e : Expr) : Lean.Meta.Grind.VarCollector

Equations

• (Int.Linear.Expr.num v).collectVars = id
• (Int.Linear.Expr.var x).collectVars = Lean.Meta.Grind.collectVar x
• a.neg.collectVars = a.collectVars
• (Int.Linear.Expr.mulL k a).collectVars = a.collectVars
• (a.mulR k).collectVars = a.collectVars
• (a.add b).collectVars = a.collectVars >> b.collectVars
• (a.sub b).collectVars = a.collectVars >> b.collectVars