Documentation

Lean.Util.CollectLooseBVars

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.

partial def Lean.Expr.CollectLooseBVars.main (e : Expr) (offset : 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
Instances For