[Agda] Observational equality model

[Conor McBride]

On 26 Apr 2010, at 10:20, Jean-Philippe Bernardy wrote:

> The authors of "Observational equality, now!" write:
>
>> We have simulated our system by a shallow embedding in Agda 2,  
>> shipping as part of the standard examples package for that system.
>
> However I can find no trace of that implementation.
> Any hint?

It did at the time...

Here's the file we had in mind. It has subsequently been broken,
but I imagine it's easily fixed. Is it still in the "old rubbish"
part of the distro, or is it gone completely?

Cheers

Conor

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ObsEq.agda
Type: application/octet-stream
Size: 8879 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100426/039078d2/ObsEq.obj
-------------- next part --------------