From ff3d12c8b57fafdfc4607867d8884259dc5d1761 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 9 Dec 2024 21:15:16 +0000 Subject: [PATCH] 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 --- src/Lean/Expr.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index f06d4e0a72..84c4b38779 100644 --- a/src/Lean/Expr.lean +++ b/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