source
def Lean.Grind.Linarith.Poly.renameVars (p : Poly) (f : Meta.Grind.VarRename) :
Poly
Equations

- Lean.Grind.Linarith.Poly.nil.renameVars f = Lean.Grind.Linarith.Poly.nil
- (Lean.Grind.Linarith.Poly.add k x p_2).renameVars f = Lean.Grind.Linarith.Poly.add k ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x) (p_2.renameVars f)

Instances For

source
def Lean.Grind.Linarith.Expr.renameVars (e : Expr) (f : Meta.Grind.VarRename) :
Expr
Equations

- Lean.Grind.Linarith.Expr.zero.renameVars f = Lean.Grind.Linarith.Expr.zero
- (Lean.Grind.Linarith.Expr.var x).renameVars f = Lean.Grind.Linarith.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)
- (Lean.Grind.Linarith.Expr.natMul k a).renameVars f = Lean.Grind.Linarith.Expr.natMul k (a.renameVars f)
- (Lean.Grind.Linarith.Expr.intMul k a).renameVars f = Lean.Grind.Linarith.Expr.intMul k (a.renameVars f)

Instances For

source
def Lean.Grind.Linarith.Poly.collectVars (p : Poly) :
Meta.Grind.VarCollector
Equations

- Lean.Grind.Linarith.Poly.nil.collectVars = id
- (Lean.Grind.Linarith.Poly.add k x p_2).collectVars = Lean.Meta.Grind.collectVar x >> p_2.collectVars

Instances For

source
def Lean.Grind.Linarith.Expr.collectVars (e : Expr) :
Meta.Grind.VarCollector
Equations

- Lean.Grind.Linarith.Expr.zero.collectVars = id
- (Lean.Grind.Linarith.Expr.var x).collectVars = Lean.Meta.Grind.collectVar x
- a.neg.collectVars = a.collectVars
- (Lean.Grind.Linarith.Expr.natMul k a).collectVars = a.collectVars
- (Lean.Grind.Linarith.Expr.intMul k a).collectVars = a.collectVars
- (a.add b).collectVars = a.collectVars >> b.collectVars
- (a.sub b).collectVars = a.collectVars >> b.collectVars

Instances For