michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/pp,library/head_map): handle 'as_atomic' annotation

Browse source 
This commit fixes local notation that contains parameters

see issue #639
This commit is contained in:
Leonardo de Moura 2015-05-29 14:51:28 -07:00
parent e6099583ad
commit a071012346
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/pp.cpp
View file

@ -871,6 +871,8 @@ bool pretty_fn::match(level const & p, level const & l) {
bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & args) {
if (is_explicit(p)) {
return match(get_explicit_arg(p), e, args);
} else if (is_as_atomic(p)) {
return match(get_app_fn(get_as_atomic_arg(p)), e, args);
} else if (is_var(p)) {
unsigned vidx = var_idx(p);
if (vidx >= args.size())

4
src/library/head_map.cpp
View file

@ -11,7 +11,9 @@ namespace lean {
head_index::head_index(expr const & e) {
expr f = get_app_fn(e);
while (true) {
if (is_explicit(f))
if (is_as_atomic(f))
f = get_app_fn(get_as_atomic_arg(f));
else if (is_explicit(f))
f = get_explicit_arg(f);
else if (is_consume_args(f))
f = get_consume_args_arg(f);