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

fix(frontends/lean/structure_instance): incorrect assertions

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-23 10:28:21 -07:00
parent 96fe057d87
commit 47b66b640f
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/brackets.cpp
View file

@ -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();

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

@ -45,7 +45,7 @@ public:
};
static expr mk_structure_instance_core(name const & s, list<name> 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);
}