The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi,

Suppose we have a simple coinductive data type:

CoInductive T : Set :=
  | A : T
  | B : T
  | C : T -> T.

Now there are terms that live in T such as

  C (C (C ... A))
  C (C (C ... B))

with infinitely many C's followed by an A or a B. However, it seems to  
me that these terms are not (constructively) definable.

Can I prove that if for [t1 t2 : T] we have [t1 <> t2], where [t1] and  
[t2] are constructively definable, then I must be able to distinguish  
between [t1] and [t2] in finite time? How can I define "constructively  
definable"?

Any pointers to relevant literature would be appreciated,

Edsko