diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean index a05ba3321c..49eae52e4d 100644 --- a/library/init/meta/pexpr.lean +++ b/library/init/meta/pexpr.lean @@ -11,6 +11,7 @@ universe u @[reducible] meta def pexpr := expr ff protected meta constant pexpr.of_expr : expr → pexpr +meta constant pexpr.is_placeholder : pexpr → bool meta constant pexpr.mk_placeholder : pexpr meta constant pexpr.mk_field_macro : pexpr → name → pexpr meta constant pexpr.mk_explicit : pexpr → pexpr diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp index 0b0b8ebb4f..2cc0d0b76c 100644 --- a/src/library/vm/vm_pexpr.cpp +++ b/src/library/vm/vm_pexpr.cpp @@ -21,6 +21,10 @@ vm_obj pexpr_of_expr(vm_obj const & e) { return to_obj(mk_as_is(to_expr(e))); } +vm_obj pexpr_is_placeholder(vm_obj const & e) { + return mk_vm_bool(is_placeholder(to_expr(e))); +} + vm_obj pexpr_mk_placeholder() { return to_obj(mk_expr_placeholder()); } @@ -52,6 +56,7 @@ vm_obj pexpr_get_structure_instance_info(vm_obj const & e) { void initialize_vm_pexpr() { DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}), pexpr_of_expr); + DECLARE_VM_BUILTIN(name({"pexpr", "is_placeholder"}), pexpr_is_placeholder); DECLARE_VM_BUILTIN(name({"pexpr", "mk_placeholder"}), pexpr_mk_placeholder); DECLARE_VM_BUILTIN(name("pexpr", "mk_explicit"), pexpr_mk_explicit);