feat(library/init/lean/expr): add Expr.hasFVar and Expr.hasMVar

cc @dselsam

library/init/lean/expr.lean

@@ -100,6 +100,12 @@ constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _
 
 instance : HasBeq Expr := ⟨Expr.eqv⟩
 
+@[extern "lean_expr_has_mvar"]
+constant hasMVar (a : @& Expr) : Bool := default _
+
+@[extern "lean_expr_has_fvar"]
+constant hasFVar (a : @& Expr) : Bool := default _
+
 def isSort : Expr → Bool
 | Expr.sort _ => true
 | _ => false

src/kernel/expr.cpp

@@ -788,6 +788,17 @@ expr infer_implicit(expr const & t, bool strict) {
     return infer_implicit(t, std::numeric_limits<unsigned>::max(), strict);
 }
 
+// =======================================
+// Extra exports
+
+extern "C" uint8 lean_expr_has_mvar(b_obj_arg o) {
+    return has_mvar(TO_REF(expr, o));
+}
+
+extern "C" uint8 lean_expr_has_fvar(b_obj_arg o) {
+    return has_fvar(TO_REF(expr, o));
+}
+
 // =======================================
 // Initialization & Finalization
 

src/util/object_ref.h

@@ -216,4 +216,7 @@ template<typename T> T get_except_value(obj_arg o) {
         throw exception(err);
     }
 }
+
+// Remark: `T` must be an `object_ref`.
+#define TO_REF(T, o) reinterpret_cast<T const &>(o)
 }

tests/lean/mvar_fvar.lean

@@ -0,0 +1,10 @@
+import init.lean
+open Lean
+
+#eval (Expr.fvar `a).hasFVar
+#eval (Expr.app (Expr.const `foo []) (Expr.fvar `a)).hasFVar
+#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasFVar
+
+#eval (Expr.mvar `a).hasMVar
+#eval (Expr.app (Expr.const `foo []) (Expr.mvar `a)).hasMVar
+#eval (Expr.app (Expr.const `foo []) (Expr.const `a [])).hasMVar

tests/lean/mvar_fvar.lean.expected.out

@@ -0,0 +1,6 @@
+true
+true
+false
+true
+true
+false