[Agda] The joys and sorrows of abstraction

[Nils Anders Danielsson]

On 2018-05-16 00:27, Philip Wadler wrote:
> Is there any way to *both* be able to compute fresh names *and* retain
> my related proofs, in particular, the proof that `fresh x xs`
> generates a name not in `xs`?

When normalising an expression you can make abstract definitions compute
by using C-u C-c C-n instead of C-c C-n. However, there is no way to
turn off abstract while type-checking (because this could lead to
problems with subject reduction).

There are other ways to control reduction. Wolfram suggested one.
Another is to match on a value of the unit type, and not supply a
concrete constructor until you want the code to compute.

-- 
/NAD