[Agda] hot computer churns codata

[Conor McBride]

Hi Andrés

On 20 May 2009, at 04:50, Andrés Sicard-Ramírez wrote:

> Hi Conor,
>
> I could type check the file disabling the termination check

Now that's funny! Thanks very much!

Many thanks. (This command line thing: is it a recent return
to the old ways? Maybe I should upgrade, but I always worry
about what else I'll have to upgrade...)

(Hmm. I just tried --no-termination-check under emacs and
got a stack overflow after about 5 minutes.)

> $ time agda --no-termination-check MTypes.agda
> Checking /tmp/MTypes.agda.
>
> Unsolved metas at the following locations:
>  /tmp/MTypes.agda:273,9-13

That's fair -- there's a hole because I can't have a postulate
in a mutual block, and I'm too lazy to do the hard work.

> real	5m11.720s
> user 5m8.907s
> sys	0m1.856s
>
> (Without to disable the termination check, I couldn't)

It's hard to see where the termination check is even being
engaged. Everything up to "finally" checks no problem, and
"finally" itself is given as an unfold, rather than by
explicit recursion. Of course, I could just take "finally"
as an axiom if I felt like it, thanks to proof-laziness.

Overall, the news is good, I think. This extensional model
seems to hang together, and it's enough to recover
dependent case analysis for codata, given just the coalgebra
presentation.

If we're really lucky, we might be able to code those nice
proofs Ralf H has been doing, proving corecursions equal
by showing they satisfy the same unfolding equation.

Thanks again

Conor