Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Universe polymorphism in the HoTT branch of Coq


Chronological Thread 
  • 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:
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).




Archive powered by MHonArc 2.6.18.

Top of Page