[Agda] Incompatibilities affecting ``Fresh Look''

[kahl at cas.mcmaster.ca]

On Tue, Dec 14, 2010 at 08:23:37AM -0800, Nicolas Pouillard wrote:
> On Mon, 13 Dec 2010 22:29:31 -0500, kahl at cas.mcmaster.ca wrote:
> > I am trying to get Nicolas Pouillard and François Pottier's ``Fresh Look''
> 
> The short answer is that since Agda and its std library is a fast moving
> target, I suggest to use the latest version available at this time.

I only found one version, namely

  http://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010.tar.gz

from:

  http://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010/


Thanks to the help from the list, I got most of this now type-checked,
with the following exceptions:

 * I commented out everything in NotSoFresh/Derived.agda
   that depends on Coinduction.

   (The current standard library still contains a Coinduction module,
    but the current Agda does not like it. And I haven't looked into
    co-induction at all, so far.)

 * NotSoFresh/Examples/Term/Conv.agda  does not go though

 * NotSoFresh/Examples/NBE-short.agda

The last two probably require more understanding of NotSoFresh,
so it will be some time before I might possibly get to them.


Attached is the (gzipped) patch with my changes. (diff -u)


Thanks again to all those who helped!


Wolfram

-------------- next part --------------
A non-text attachment was scrubbed...
Name: pouillard-pottier-fresh-look-agda_WK2010-12-15.patch.gz
Type: application/octet-stream
Size: 3925 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20101215/332c3bfd/pouillard-pottier-fresh-look-agda_WK2010-12-15.patch.obj