coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: roconnor AT theorem.ca
- To: Coq Club <coq-club AT pauillac.inria.fr>
- Cc: Conor McBride <conor AT strictlypositive.org>
- Subject: Re: [Coq-Club] Coinductive types and type preservation.
- Date: Sat, 7 Jun 2008 02:18:37 -0400 (EDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Fri, 6 Jun 2008, Conor McBride wrote:
Definition p : ones = cons ones
Canonicity tells us that p's type should not
be inhabited.
Why shouldn't ones and (cons ones) be convertable? Can't we just expand the cofixpoint of ones until the same number of constructors are exposed as is in (cons ones), and then compare the resulting terms?
I'm probably being naive here.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
- [Coq-Club] Coinductive types and type preservation., Nicolas Oury
- Re: [Coq-Club] Coinductive types and type preservation.,
Conor McBride
- Re: [Coq-Club] Coinductive types and type preservation.,
Arnaud Spiwack
- Re: [Coq-Club] Coinductive types and type preservation., Conor McBride
- Re: [Coq-Club] Coinductive types and type preservation., Nicolas Oury
- Re: [Coq-Club] Coinductive types and type preservation., roconnor
- Re: [Coq-Club] Coinductive types and type preservation.,
Conor McBride
- Re: [Coq-Club] Coinductive types and type preservation.,
roconnor
- Re: [Coq-Club] Coinductive types and type preservation.,
roconnor
- Re: [Coq-Club] Coinductive types and type preservation.,
Bruno Barras
- Re: [Coq-Club] Coinductive types and type preservation., Thorsten Altenkirch
- Re: [Coq-Club] Coinductive types and type preservation.,
Bruno Barras
- Re: [Coq-Club] Coinductive types and type preservation., roconnor
- Re: [Coq-Club] Coinductive types and type preservation.,
roconnor
- Re: [Coq-Club] Coinductive types and type preservation.,
roconnor
- Re: [Coq-Club] Coinductive types and type preservation.,
Conor McBride
- Re: [Coq-Club] Coinductive types and type preservation.,
Arnaud Spiwack
- Re: [Coq-Club] Coinductive types and type preservation., Adam Chlipala
- Re: [Coq-Club] Coinductive types and type preservation., Carlos . SIMPSON
- Re: [Coq-Club] Coinductive types and type preservation.,
Conor McBride
Archive powered by MhonArc 2.6.16.