The Coq mailing list

[roconnor AT theorem.ca]

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.''