From d03e00de99096689a1504312c01fe6af06b2fda9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jul 2019 13:37:01 -0700 Subject: [PATCH] chore(frontends/lean/builtin_exprs): remove obsolete notation from old parser --- src/frontends/lean/builtin_exprs.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 2a5a350b66..b187a76434 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -838,20 +838,9 @@ parse_table init_nud_table() { return r; } -static expr parse_field(parser & p, unsigned, expr const * args, pos_info const & pos) { - if (p.curr_is_numeral()) { - unsigned fidx = p.parse_small_nat(); - return p.save_pos(mk_field_notation(args[0], fidx), pos); - } else { - name field = p.check_id_next("identifier or numeral expected"); - return p.save_pos(mk_field_notation(args[0], field), pos); - } -} - parse_table init_led_table() { parse_table r(false); r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(mk_bvar(1), mk_bvar(1))); - r = r.add({transition("^.", mk_ext_action(parse_field))}, mk_bvar(0)); return r; }