Given an expression e = fun (x₁ : α₁) .. (xₙ : αₙ) => b
, runs f
on each αᵢ
and b
.
Equations
- Lean.Meta.visitLambda f e = Lean.Meta.visitLambda.visit f #[] e
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.visitLambda.visit f fvars x✝ = f (x✝.instantiateRev fvars)
Instances For
Given an expression e = (x₁ : α₁) → .. (xₙ : αₙ) → b
, runs f
on each αᵢ
and b
.
Equations
- Lean.Meta.visitForall f e = Lean.Meta.visitForall.visit f #[] e
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.visitForall.visit f fvars x✝ = f (x✝.instantiateRev fvars)
Instances For
Given a sequence of let binders let (x₁ : α₁ := v₁) ... in b
, runs f
on each αᵢ
, vᵢ
and b
.
Equations
- Lean.Meta.visitLet f e = Lean.Meta.visitLet.visit f #[] e
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.visitLet.visit f fvars x✝ = f (x✝.instantiateRev fvars)
Instances For
Similar to Expr.forEach'
, but creates free variables whenever going inside of a binder.
If the inner function returns false
, deeper subexpressions will not be visited.
Equations
- Lean.Meta.forEachExpr' input fn = (Lean.Meta.forEachExpr'.visit fn { } { monadLift := fun {α : Type} (x : ST IO.RealWorld α) => liftM (liftM x) } input).run
Instances For
Similar to Expr.forEach
, but creates free variables whenever going inside of a binder.
Equations
- Lean.Meta.forEachExpr e f = Lean.Meta.forEachExpr' e fun (e : Lean.Expr) => do f e pure true
Instances For
Auxiliary method for (temporarily) setting the user facing name of metavariables.
Let ?m
be a metavariable in isTarget.contains ?m
, and ?m
does not have a user facing name.
Then, we try to find an application f ... ?m
in e
, and (temporarily) use the
corresponding parameter name (with a fresh macro scope) as the user facing name for ?m
.
This method returns all metavariables whose user facing name has been updated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Remove user facing name for metavariables in toReset
.
This a low-level method for "undoing" the effect of setMVarUserNamesAt
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to mkForallFVars
, but tries to infer better binder names when xs
contains metavariables.
Let ?m
be a metavariable in xs
s.t. ?m
does not have a user facing name.
Then, we try to find an application f ... ?m
in the other binder typer and type
, and
(temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for ?m
.
The "renaming" is temporary.
Equations
- One or more equations did not get rendered due to their size.