source
def Lean.Grind.AC.Seq.renameVars (s : Seq) (f : Meta.Grind.VarRename) :
Seq
Equations

- (Lean.Grind.AC.Seq.var x).renameVars f = Lean.Grind.AC.Seq.var ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x)
- (Lean.Grind.AC.Seq.cons x s_2).renameVars f = Lean.Grind.AC.Seq.cons ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x) (s_2.renameVars f)

Instances For

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

- (Lean.Grind.AC.Expr.var x).renameVars f = Lean.Grind.AC.Expr.var ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x)
- (a.op b).renameVars f = (a.renameVars f).op (b.renameVars f)

Instances For

source
def Lean.Grind.AC.Seq.collectVars (s : Seq) :
Meta.Grind.VarCollector
Equations

- (Lean.Grind.AC.Seq.var x).collectVars = Lean.Meta.Grind.collectVar x
- (Lean.Grind.AC.Seq.cons x s_2).collectVars = Lean.Meta.Grind.collectVar x >> s_2.collectVars

Instances For

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

- (Lean.Grind.AC.Expr.var x).collectVars = Lean.Meta.Grind.collectVar x
- (a.op b).collectVars = a.collectVars >> b.collectVars

Instances For