[Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes

[Nils Anders Danielsson]

On 2012-04-23 17:43, James Deikun wrote:
> Indeed.  I can't say for sure that it's sound, but at least the one
> major issue I thought of (that termination checking might see that the
> recursive calls are thrown away and admit proofs that wouldn't terminate
> with 'hideProof = id') doesn't seem to be a problem from my testing.
> (I'm not sure that it won't show up in sufficiently complex mutual
> recursions, though.)

Beta-redexes are reduced before the termination-checker is run
(http://code.google.com/p/agda/issues/detail?id=497), so you can get
into trouble if you inline hideProof:

   2+2≡5 : 2 + 2 ≡ 5
   2+2≡5 = (λ (_ : 2 + 2 ≡ 5) → trustMe ∶ 2 + 2 ≡ 5) 2+2≡5

> I had heard that something like this might come out of the last AIM;
> is there any work in progress?

No, I don't think so.

-- 
/NAD