max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(init/meta/pexpr): expose pexpr.is_placeholder

Browse source
This commit is contained in:
Sebastian Ullrich 2017-08-26 23:21:44 +02:00
parent 2e5284add7
commit 07d8b18caf
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/meta/pexpr.lean
View file

@ -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

5
src/library/vm/vm_pexpr.cpp
View file

@ -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);