michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-05 11:55:41 -08:00
parent d6dc624ca8
commit 677e0aeef6
2 changed files with 20 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/structure_cmd.cpp
View file

@ -213,11 +213,18 @@ struct structure_cmd_fn {
m_type = m_p.parse_expr();
if (!is_sort(m_type))
throw parser_error("invalid 'structure', 'Type' expected", pos);
if (has_placeholder(m_type))
throw_explicit_universe(pos);
level l = sort_level(m_type);
if (m_env.impredicative() && !is_not_zero(l))
throw parser_error("invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment", pos);
if (m_infer_result_universe) {
if (!is_placeholder(sort_level(m_type)))
throw parser_error("invalid 'structure', resultant universe level is computed "
"automatically when universe level parameters are not provided", pos);
} else {
if (has_placeholder(m_type))
throw_explicit_universe(pos);
level l = sort_level(m_type);
if (m_env.impredicative() && !is_not_zero(l))
throw parser_error("invalid 'structure', the resultant universe level should not be zero "
"for any universe parameter assignment", pos);
}
} else {
if (!m_infer_result_universe)
throw_explicit_universe(pos);

8
tests/lean/run/record9.lean Normal file
View file

@ -0,0 +1,8 @@
import logic
constant fibrant : Type → Prop
structure Fib : Type :=
{type : Type} (pred : fibrant type)
check Fib.mk