[Agda] Observational equality model

[Jean-Philippe Bernardy]

Given the file name I can now see it:

./examples/outdated-and-incorrect/OTT/ObsEq.agda
./examples/outdated-and-incorrect/OTT/ObsEq2.agda

... with at least textual differences to the version you just sent.

Thanks!
-- JP

On Mon, Apr 26, 2010 at 11:31 AM, Conor McBride
<conor at strictlypositive.org> wrote:
>
> 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
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>