coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewriting with the cousin of iff on types

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] rewriting with the cousin of iff on types
Date: Fri, 23 Aug 2013 20:02:43 +0200

On 23/08/2013 19:58, Abhishek Anand wrote:
> It looks like the setoid mechanism wont work for the t_iff relation because
> it is a relation that lives in Type.

There is an open bug in the bugtracker for this issue:

https://coq.inria.fr/bugs/show_bug.cgi?id=2440

I've been told that it would be fixed by the introduction of universe
polymorphism that should be around by the 8.5 version (already in the
HoTT branch). So, basically, for the moment, be patient.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] rewriting with the cousin of iff on types, Abhishek Anand, 08/23/2013
- Re: [Coq-Club] rewriting with the cousin of iff on types, Pierre-Marie Pédrot, 08/23/2013
  - Re: [Coq-Club] rewriting with the cousin of iff on types, Abhishek Anand, 08/24/2013
    - Re: [Coq-Club] rewriting with the cousin of iff on types, Abhishek Anand, 08/26/2013
      - Re: [Coq-Club] rewriting with the cousin of iff on types, Rui Baptista, 08/26/2013
        
        Re: [Coq-Club] rewriting with the cousin of iff on types, Abhishek Anand, 08/27/2013