[Agda] My coinductive function doesn't termination-check

[Nick Smallbone]

On 18 October 2011 15:20, Ulf Norell <ulf.norell at gmail.com> wrote:
>>  data Delay (A : Set) : Set where
>>    now : A → Delay A
>>    later : ∞ (Delay A) → Delay A
>>
>>  fix : ∀ {A} → (Delay A → Delay A) → Delay A
>>  fix f = later (♯ f (fix f))
>>
>> The idea is that Delay A represents a computation that may eventually
>> produce a value of type A---or might not. As I understand it, fix is
>> productive, but it doesn't seem to termination-check. Why's that?
>
> What if f is
> f (later x) = ♭ x
> f (now x) = now x
> ?

Ah, you're right! f (fix f) reduces to f (fix f). Silly me.

Nick