From db71a29c813009c599bc5d4009b271c898c8a7b3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Feb 2015 12:22:17 -0800 Subject: [PATCH] feat(frontends/lean/parse_rewrite_tactic): improve esimp tactic --- src/frontends/lean/parse_rewrite_tactic.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 5343097aa..56fee9a26 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -32,9 +32,7 @@ static expr parse_rule(parser & p) { } } -static expr parse_rewrite_unfold(parser & p) { - lean_assert(p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())); - p.next(); +static expr parse_rewrite_unfold_core(parser & p) { buffer to_unfold; if (p.curr_is_token(get_lcurly_tk())) { p.next(); @@ -52,6 +50,12 @@ static expr parse_rewrite_unfold(parser & p) { return mk_rewrite_unfold(to_list(to_unfold), loc); } +static expr parse_rewrite_unfold(parser & p) { + lean_assert(p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())); + p.next(); + return parse_rewrite_unfold_core(p); +} + expr parse_rewrite_element(parser & p) { if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) return parse_rewrite_unfold(p); @@ -138,6 +142,8 @@ expr parse_esimp_tactic(parser & p) { buffer elems; if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) { elems.push_back(parse_rewrite_unfold(p)); + } else if (p.curr_is_token(get_lcurly_tk())) { + elems.push_back(parse_rewrite_unfold_core(p)); } else { location loc = parse_tactic_location(p); elems.push_back(mk_rewrite_reduce(loc));