Smart Case [Re: [Agda] A puzzle with "with"]

[Ulf Norell]

> @Nisse:  Surely, Agda expressions could not be translated to core
> anymore, but their typing derivations could.  For instance, into a
> language with explicit proofs of definitional equality everywhere, as
> suggested by Freek Wiedijk.
>

"With" is easily explainable as a local function, and Agda generates and
type checks this function when checking a with.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090703/149484f8/attachment.html