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

fix(frontends/lean/structure_cmd): handle is_one_placeholder

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-02 08:07:19 -07:00
parent 96538ba899
commit f21f1219d9
4 changed files with 26 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -254,6 +254,9 @@ struct structure_cmd_fn {
m_inductive_predicate = is_zero(sort_level(m_type));
if (m_inductive_predicate) {
m_infer_result_universe = false;
} else if (is_one_placeholder(sort_level(m_type))) {
m_infer_result_universe = false;
m_type = m_p.save_pos(mk_sort(mk_level_one()), pos);
} else {
m_infer_result_universe = is_placeholder(sort_level(m_type));
if (!m_infer_result_universe) {

6
tests/lean/bad_structures.lean
View file

@ -1,12 +1,12 @@
prelude namespace foo structure {l} prod (A : Type l) (B : Type l) :=
(pr1 : A) (pr2 : B)
structure {l} prod (A : Type l) (B : Type l) : Type :=
structure {l} prod1 (A : Type l) (B : Type l) : Type :=
(pr1 : A) (pr2 : B)
structure {l} prod (A : Type l) (B : Type l) : Type l :=
structure {l} prod2 (A : Type l) (B : Type l) : Type l :=
(pr1 : A) (pr2 : B)
structure {l} prod2 (A : Type l) (B : Type l) : Type (max 1 l) :=
structure {l} prod3 (A : Type l) (B : Type l) : Type (max 1 l) :=
(pr1 : A) (pr2 : B)
end foo

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

@ -1,2 +1,2 @@
bad_structures.lean:4:52: 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')
bad_structures.lean:7:54: 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')
bad_structures.lean:4:0: error: universe level of type_of(arg #3) of 'foo.prod1.mk' is too big for the corresponding inductive datatype
bad_structures.lean:7:55: 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')

18
tests/lean/run/structure_result_universe.lean Normal file
View file

@ -0,0 +1,18 @@
structure foo1 (A : Type) : Type :=
(elt : A)
structure {u} foo2 (A : Type u) : Type (u+1) :=
(val : A)
structure {u} foo3 (A : Type u) : Type (max u 1) :=
(val : A)
universe variable u
structure foo4 (A : Type u) : Type (max u 1) :=
(val : A)
check foo1
check foo2
check foo3
check foo4