coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: vincent rahli <vincent.rahli AT gmail.com>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq
- Date: Thu, 5 Sep 2013 19:36:48 -0400
Please report this bug at https://github.com/HoTT/coq/issues/new. This might be related to https://github.com/HoTT/coq/issues/53. If you [Set Printing Universes.], you will see that it is failing to unify [Type] with [Set]. As a work-around, you can replace "list nat" with "list (nat : Type)". Also, you can use "Set Universe Polymorphism" rather than using "Polymorphic" everywhere.
-Jason
On Thursday, September 5, 2013, vincent rahli wrote:
On Thursday, September 5, 2013, vincent rahli wrote:
Hi,We're trying to use the HoTT branch of Coq (downloaded today) in order to get
universe polymorphism.Unfortunately we keep on running into this error [Error: Universe inconsistency],
which is the very error we were trying to avoid by using the HoTT branch of Coq.One of our problems is that [try] does not catch this error (see the code below).- Why doesn't [try] catch that error?
- Why do we get a universe inconsistency error here and not
[Error: Unable to unify.] (without the [try])?Thanks.Vincent & Abhishek.
-----------------------------------------------------------------------------------------
Require Export Coq.Lists.List.
Polymorphic Fixpoint LIn (A : Type) (a:A) (l:list A) : Type :=
match l with
| nil => False
| b :: m => (b = a) + LIn A a m
end.
Polymorphic Inductive NTerm : Type :=
| cterm : NTerm
| oterm : list NTerm -> NTerm.
Polymorphic Fixpoint dummy {A B} (x : list (A * B)) : list (A * B) :=
match x with
| nil => nil
| (_, _) :: _ => nil
end.
Lemma foo :
forall v t sub vars,
LIn (nat * NTerm) (v, t) (dummy sub)
->
(
LIn (nat * NTerm) (v, t) sub
*
notT (LIn nat v vars)
).
Proof.
induction sub; simpl; intros.
destruct H.
try (apply IHsub in X).
- [Coq-Club] Universe polymorphism in the HoTT branch of Coq, vincent rahli, 09/06/2013
- Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq, Jason Gross, 09/06/2013
- Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq, Matthieu Sozeau, 09/06/2013
- Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq, Jason Gross, 09/07/2013
- Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq, vincent rahli, 09/07/2013
Archive powered by MHonArc 2.6.18.