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

fix: syntax for universe parameters in axiom

Browse source
This commit is contained in:
Sebastian Ullrich 2019-10-08 18:11:37 +02:00
parent 90fc2b7d39
commit ef6853979f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -248,8 +248,8 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const
throw parser_error("invalid declaration, only axioms can be universe polymorphic", p.pos());
if (k == variable_kind::Axiom)
scope1.emplace(p);
parse_univ_params(p, ls_buffer);
n = p.check_decl_id_next("invalid declaration, identifier expected");
parse_univ_params(p, ls_buffer);
if (!p.curr_is_token(get_colon_tk())) {
if (!curr_is_binder_annotation(p) && (k == variable_kind::Variable)) {
p.parse_close_binder_info(bi);