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

[Nils Anders Danielsson]

On 2012-04-18 22:48, James Deikun wrote:
> Needless recursion when building or verifying equalities is prevented
> using the following function, which throws away its argument while
> requiring a suitable proof of said argument's existence:
>
> >  hideProof : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y
> >  hideProof eq = trustMe

Nice trick. I wonder if it's sound. If it is sound, then we should
perhaps try to find a less hacky way to do this.

> The pairing heap (Heap.agda) and sieve (Sieve.agda) implementations use
> pattern-matching as a sequentialization measure to control duplication
> of unevaluated thunks, which can cause an exponential slowdown.

We should really switch to a more efficient evaluation strategy.

-- 
/NAD