From 47b66b640f5d1bc49ba51bdbcaa47f37c40c64e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2016 10:28:21 -0700 Subject: [PATCH] fix(frontends/lean/structure_instance): incorrect assertions --- src/frontends/lean/brackets.cpp | 2 +- src/frontends/lean/structure_instance.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp index d9dd048cbc..74096a61ad 100644 --- a/src/frontends/lean/brackets.cpp +++ b/src/frontends/lean/brackets.cpp @@ -36,7 +36,7 @@ static expr mk_singleton(parser & p, pos_info const & pos, expr const & e) { /* Parse rest of the insertable '{' expr ... */ static expr parse_insertable(parser & p, pos_info const & pos, expr const & e) { - lean_assert(p.curr_is_token(get_comma_tk())); + lean_assert(p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_rcurly_tk())); expr r = mk_singleton(p, pos, e); while (p.curr_is_token(get_comma_tk())) { auto ins_pos = p.pos(); diff --git a/src/frontends/lean/structure_instance.cpp b/src/frontends/lean/structure_instance.cpp index ca4dd7ed8a..5aac95b09f 100644 --- a/src/frontends/lean/structure_instance.cpp +++ b/src/frontends/lean/structure_instance.cpp @@ -45,7 +45,7 @@ public: }; static expr mk_structure_instance_core(name const & s, list const & fs, unsigned num, expr const * args) { - lean_assert(num == length(fs) && num == length(fs) + 1); + lean_assert(num == length(fs) || num == length(fs) + 1); macro_definition def(new structure_instance_macro_cell(s, fs)); return mk_macro(def, num, args); }