[Agda] Running a classical proof with choice in Agda

[Nils Anders Danielsson]

On 2011-05-09 13:08, Martin Escardo wrote:
> I take the opportunity to make a general Agda question, that hopefully
> somebody in the Agda list can answer. In order to try to make
> ProgramsWithoutSpecification.agda compile, I tried to replace the
> definition of J-∀-shift-selection in the module
> Infinite-J-Shift-Selection.agda by a postulate, assuming that evaluation
> would stop when the uninterpreted term J-∀-shift-selection is
> encountered. However, with this not only
> ProgramsWithoutSpecification.agda still doesn't compile, but also
> Examples.agda now fails to compile!

The introduction of the postulate may have meant that huge "thunks"
started building up in the heap.

-- 
/NAD