coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Chlipala <adam AT chlipala.net>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal.
Date: Wed, 17 Feb 2010 13:17:04 -0500

Vladimir Voevodsky wrote:

They should be equal because they translate into the same terms in the
calculus of inductive constructions.

The crucial fact here is that Coq is based on Gallina, not the literal CIC. Gallina has datatype generativity, just like ML does.

[Coq-Club] hint database pollution, Damien Pous
- Re: [Coq-Club] hint database pollution, Pierre Letouzey
  - Re: [Coq-Club] hint database pollution, Damien Pous
- [Coq-Club] how to make Coq to recognize that two inductive definitions are equal., Vladimir Voevodsky
  - Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal., Adam Chlipala
    - Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal., Vladimir Voevodsky
      - Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal., Adam Chlipala
        
        Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal., Vladimir Voevodsky