feat: expose hasLooseBVar

library/Init/Lean/Expr.lean

@@ -319,6 +319,9 @@ constant getLooseBVarRange (e : @& Expr) : Nat := arbitrary _
 def hasLooseBVars (e : Expr) : Bool :=
 getLooseBVarRange e > 0
 
+@[extern "lean_expr_has_loose_bvar"]
+constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool := arbitrary _
+
 /-- Instantiate the loose bound variables in `e` using `subst`.
     That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
 @[extern "lean_expr_instantiate"]

src/kernel/expr.cpp

@@ -805,6 +805,12 @@ bool has_loose_bvar(expr const & e, unsigned i) {
     return found;
 }
 
+extern "C" uint8 lean_expr_has_loose_bvar(b_obj_arg e, b_obj_arg i) {
+    if (!lean_is_scalar(i))
+        return false;
+    return has_loose_bvar(TO_REF(expr, e), lean_unbox(i));
+}
+
 expr lower_loose_bvars(expr const & e, unsigned s, unsigned d) {
     if (d == 0 || s >= get_loose_bvar_range(e))
         return e;

tests/lean/run/expr1.lean

@@ -37,3 +37,24 @@ do let f   := Expr.const `f [];
    pure ()
 
 #eval tst3
+
+
+def tst4 : IO Unit :=
+do let f   := Expr.const `f [];
+   let a   := Expr.const `a [];
+   let b   := Expr.const `b [];
+   let x0   := Expr.bvar 0;
+   let x1   := Expr.bvar 1;
+   let t1   := mkApp f #[a, b];
+   let t2   := mkApp f #[a, x0];
+   let t3   := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkApp f #[a, x0]);
+   let t4   := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkApp f #[a, x1]);
+   unless (!t1.hasLooseBVar 0) $ throw "failed-1";
+   unless (t2.hasLooseBVar 0) $ throw "failed-2";
+   unless (!t3.hasLooseBVar 0) $ throw "failed-3";
+   unless (t4.hasLooseBVar 0) $ throw "failed-4";
+   unless (!t4.hasLooseBVar 1) $ throw "failed-4";
+   unless (!t2.hasLooseBVar 1) $ throw "failed-5";
+   pure ()
+
+#eval tst4