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

feat(frontends/lean/util): elaborate priority/precedence expressions using the new elaborator

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-03 17:00:24 -07:00
parent aeafe0293b
commit b6be493cef
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -47,7 +47,7 @@ static unsigned parse_precedence_core(parser & p) {
parser::local_scope scope(p, env);
expr pre_val = p.parse_expr(get_max_prec());
pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val);
expr val = std::get<0>(p.old_elaborate(pre_val, list<expr>()));
expr val = p.elaborate(list<expr>(), pre_val).first;
val = normalize(p.env(), val);
if (optional<mpz> mpz_val = to_num_core(val)) {
if (!mpz_val->is_unsigned_int())

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

@ -473,7 +473,7 @@ optional<unsigned> parse_priority(parser & p) {
auto pos = p.pos();
expr pre_val = p.parse_expr();
pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val);
expr val = std::get<0>(p.old_elaborate(pre_val, list<expr>()));
expr val = p.elaborate(list<expr>(), pre_val).first;
val = normalize(p.env(), val);
if (optional<mpz> mpz_val = to_num_core(val)) {
if (!mpz_val->is_unsigned_int())