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

fix(src/frontends/lean/structure_cmd): fixes #1036

Browse source
This commit is contained in:
Daniel Selsam 2016-04-16 09:56:41 -07:00 • committed by Leonardo de Moura
parent 4fdf608c36
commit aabdabdb17
4 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -262,6 +262,13 @@ struct structure_cmd_fn {
} else {
if (has_placeholder(m_type))
throw_explicit_universe(pos);
// Note that if we do infer the result universe, `mk_result_level` will ensure that the
// result type cannot be zero when the structure might otherwise eliminate only to zero.
if (m_env.impredicative() && !is_zero(sort_level(m_type)) && !is_not_zero(sort_level(m_type)))
throw parser_error("invalid universe polymorphic structure declaration, "
"the resultant universe is not Prop (i.e., 0), "
"but it may be Prop for some parameter values "
"(solution: use 'l+1' or 'max 1 l')", m_p.pos());
}
} else {
if (!m_infer_result_universe)

1
tests/lean/bad_structures.lean.expected.out
View file

@ -1,2 +1,3 @@
bad_structures.lean:1:71: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
bad_structures.lean:7:60: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')

1
tests/lean/structure_result_type_may_be_zero.lean Normal file
View file

@ -0,0 +1 @@
record Fun.{uA uB} (A : Type.{uA}) (B : Type.{uB}) : Type.{imax uA uB} := (item : Π(a : A), B)

1
tests/lean/structure_result_type_may_be_zero.lean.expected.out Normal file
View file

@ -0,0 +1 @@
structure_result_type_may_be_zero.lean:1:71: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')