[Agda] Running a classical proof with choice in Agda

[Martin Escardo]

On 09/05/11 12:38, Nils Anders Danielsson wrote:
> The introduction of the postulate may have meant that huge "thunks"
> started building up in the heap.

Is there any way around this?

Also, I suspect that the original ProgramsWithoutSpecification.agda 
should strongly normalize (despite what I said earlier), because it is 
the same things as the main "theorem", with the proof obligations 
projected out.

Martin