diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 139ddb264..21de1da90 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -832,12 +832,12 @@ void parser::parse_binders_core(buffer & r, buffer * nentr } local_environment parser::parse_binders(buffer & r, buffer * nentries, - bool & last_block_delimited) { + bool & last_block_delimited, bool allow_empty) { flet save(m_env, m_env); // save environment local_expr_decls::mk_scope scope(m_local_decls); unsigned old_sz = r.size(); parse_binders_core(r, nentries, last_block_delimited); - if (old_sz == r.size()) + if (!allow_empty && old_sz == r.size()) throw_invalid_open_binder(pos()); return local_environment(m_env); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d1cb9568d..457f59e93 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -185,7 +185,7 @@ class parser { expr parse_binder_core(binder_info const & bi); void parse_binder_block(buffer & r, binder_info const & bi); void parse_binders_core(buffer & r, buffer * nentries, bool & last_block_delimited); - local_environment parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited); + local_environment parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited, bool allow_empty = false); bool parse_local_notation_decl(buffer * entries); friend environment section_cmd(parser & p); @@ -328,6 +328,9 @@ public: local_environment parse_binders(buffer & r) { bool tmp; return parse_binders(r, nullptr, tmp); } + local_environment parse_optional_binders(buffer & r) { + bool tmp; return parse_binders(r, nullptr, tmp, true); + } local_environment parse_binders(buffer & r, buffer & nentries) { bool tmp; return parse_binders(r, &nentries, tmp); } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 572261c12..a96665f22 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -416,7 +416,7 @@ struct structure_cmd_fn { void parse_new_fields(buffer & new_fields) { parser::local_scope scope(m_p); add_locals(); - m_p.parse_binders(new_fields); + m_p.parse_optional_binders(new_fields); check_new_field_names(new_fields); } @@ -704,7 +704,8 @@ struct structure_cmd_fn { m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); m_mk = m_name + m_mk; m_mk_infer = parse_implicit_infer_modifier(m_p); - m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected"); + if (!m_p.curr_is_command_like()) + m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected"); } process_new_fields(); } else { diff --git a/tests/lean/run/record5.lean b/tests/lean/run/record5.lean new file mode 100644 index 000000000..6811a2232 --- /dev/null +++ b/tests/lean/run/record5.lean @@ -0,0 +1,18 @@ +import logic data.unit + +structure point (A : Type) (B : Type) := +mk :: (x : A) (y : B) + +structure point2 (A : Type) (B : Type) extends point A B := +make + +check point2.make + +structure point3 extends point num num, point2 num num renaming x→y y→z + +check point3.mk + +set_option pp.coercions true + +theorem tst : point3.mk 1 2 3 = point2.make 2 3 := +rfl