doc: clarify difference between Expr.hasLooseBVars and Expr.hasLooseBVar (#6344)

This PR adds docstrings to `Expr.hasLooseBVars` and `Expr.hasLooseBVar`,
to clarify the difference between these functions, and to document that
the former traverses the expression, while the latter is constant-time,
using cached information.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Expr.lean

@@ -1235,6 +1235,9 @@ def getRevArg!' : Expr → Nat → Expr
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀
 
+/-- Return `true` if `e` contains any loose bound variables.
+
+This is a constant time operation. -/
 def hasLooseBVars (e : Expr) : Bool :=
   e.looseBVarRange > 0
 
@@ -1247,6 +1250,11 @@ def isArrow (e : Expr) : Bool :=
   | forallE _ _ b _ => !b.hasLooseBVars
   | _ => false
 
+/--
+Return `true` if `e` contains the specified loose bound variable with index `bvarIdx`.
+
+This operation traverses the expression tree.
+-/
 @[extern "lean_expr_has_loose_bvar"]
 opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool