The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

> CoInductive clock: Set := Tick (_ : clock).
> CoFixpoint ticks := Tick ticks.
> Definition foo := let: Tick _ as t := ticks return t = t in refl_equal _.
> Definition fubar := Eval compute in Some foo. (* Type error !! *)
> (** I fixed some typo :) **)

The error message says: 

"Tick (cofix ticks  : clock := Tick ticks) =
 Tick (cofix ticks  : clock := Tick ticks)" which should be coercible to
"(cofix ticks  : clock := Tick ticks) = (cofix ticks  : clock := Tick ticks)"

I could think the two terms are extensionally equal.

I have been looking for a way to forbid the intentional equality 
on colists at all so that any predicate on colists shall not distinguish 
bisimilar colists. That's why I am interested in "Add Relation colists 
bisimilar". 
Having a deep-embedded predicate language would be an option, which I am not
sure if I want.

Kind regards,
Keiko