Collecting set of loose bound variables #
This module provides a function for collecting the set of loose bvars in an expression.
This means finding the set of i
for which e.hasLooseBVar i
is true.
- visited : Std.HashSet (Nat × Expr)
- bvars : Std.HashSet Nat
Instances For
@[reducible, inline]
Instances For
Collects the loose bound variables in e
with indices at least offset
.
Returns a set of indices relative to offset
.
Specification: i ∈ e.collectLooseBVars offset ↔ e.hasLooseBVar (i + offset)
.
Equations
- e.collectLooseBVars offset = if e.hasLooseBVars = true then match StateT.run (Lean.Expr.CollectLooseBVars.main e offset) { } with | (fst, s) => s.bvars else ∅