search

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

"Check (nat : Type) : Set." now fails with universe inconsistency (polyproj) #103

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago 
Check (nat : Type) : Set.
(* Error:
The term "nat:Type" has type "Type" while it is expected to have type
"Set" (Universe inconsistency). *)
mattam82 commented 10 years ago

This makes sense, that Type has a rigid universe level and hence can't be coerced to Set. This is backwards-compatible as well.

mattam82 commented 10 years ago

Also, how am I supposed to disallow the unification of @eq Type A B and @eq Set A B from another bug report if this is allowed?

JasonGross commented 10 years ago

Er, right. I think this worked in HoTT/coq, but I agree now that it shouldn't. Feel free to move the corresponding test case from opened to closed, leaving the Fail in place, so that we have a test that this shouldn't work.