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.

structure Lean.Expr.CollectLooseBVars.State : Type

• visited : Std.HashSet (Nat × Expr)
• bvars : Std.HashSet Nat

@[reducible, inline]

abbrev Lean.Expr.CollectLooseBVars.M (α : Type) : Type

Equations

• Lean.Expr.CollectLooseBVars.M = StateM Lean.Expr.CollectLooseBVars.State

partial def Lean.Expr.CollectLooseBVars.main (e : Expr) (offset : Nat) : M Unit

def Lean.Expr.collectLooseBVars (e : Expr) (offset : Nat := 0) : Std.HashSet Nat

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 ∅