[Agda] Dealing with HOAS

[Darin Morrison]

On Sat, Sep 26, 2009 at 1:43 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> On 2009-09-26 12:50, Darin Morrison wrote:
>>
>> Below I've included code for the first part I described.
>
> I have code which includes the "second part". (And PHOAS as well.)
> Almost no proofs, though.

Very nice, thanks.

I have a slightly different version here:

http://www.cs.nott.ac.uk/~dwm/nbe/html/NBE.html

and

http://www.cs.nott.ac.uk/~dwm/nbe/nbe.zip

There's the start of a correctness proof but I stopped since I think I
came up with a nicer way to do it, although I never actually got
around to it... :)

Cheers,
Darin