How best to determine if an Expr has loose bvars?

Stream: lean4 dev

[Alex Keizer]

While reviewing lean4#5657, the question came up if Expr.data also caches whether an expression has loose bvars or not.

A doc search came up with Expr.hasLooseBVars and Expr.hasLooseBVar (notice the lack of s). The former is an extern function, and (based on a cursory glance) the C++ code seems to traverse the expression, while the latter just checks a field from Expr.data and should thus be cached, correct?

My question thus:

• It seems to me these functions should always return the same result, is that true?
• Based on the fact that hasLooseBVar is cached, and hasLooseBVars is not, is there a reason to use/prefer the latter? Should we add a docstring to the pointing out it isn't cached, and linking to the former?

[Sebastian Ullrich]

Hint: these two functions do not have the same signature :)

[Alex Keizer]

Ahhh, right, the lack of s is actually significant!

[Alex Keizer]

For future reference: Expr.hasLooseBVar also takes in a bvarIdx, and presumably checks for presence of the specified bvar? Whereas hasLooseBVars just returns whether any loose bvars exists

[Sebastian Ullrich]

yes

[Alex Keizer]

I opened a PR to add docstrings to this effect: https://github.com/leanprover/lean4/pull/6344