Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coinductive types and type preservation.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coinductive types and type preservation.


chronological Thread 
  • 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.''





Archive powered by MhonArc 2.6.16.

Top of Page