Map Fusion for Nested Datatypes in Intensional Type Theory

All the following code is additional material to the article of the same name by the author that appeared in Science of Computer Programming, Elsevier, Vol.76, pp.204-224, 2011.

The following version of the code was put here on February 2, 2010.

LNMItPred.v (Version 2.7)
LNMItImp.v (Version 2.5)
LNGMItPred.v (Version 1.5)
LNGMItImp.v (Version 1.3a)
LamFlatPred.v (Version 1.1)
README.txt
PDF of coqdoc of predicative development (first, third and fifth file)
PDF of coqdoc of impredicative development (second and fourth file)
a ZIP file with everything

The old MPC'08 development is here.

Update for Coq 8.4

LNMItPred.v (Version 2.9.1)
LNMItImp.v (Version 2.6)
LNGMItPred.v (Version 1.7)
LNGMItImp.v (Version 1.4)
LamFlatPred.v (Version 1.3.1)
README.txt
a ZIP file with these six files

All tested with Coq 8.4pl1 (December 2012). Still compiles fine with Coq 8.4pl6 (July 2015).

Update for Coq 8.5

LNMItPred.v (Version 2.9.1)
LNMItImp.v (Version 2.6)
LNGMItPred.v (Version 1.7.1)
LNGMItImp.v (Version 1.4)
LamFlatPred.v (Version 1.3.1)
README.txt
a ZIP file with these six files

All tested with Coq 8.5pl1 (April 2016).

There is also a ZIP file with the six files that profits from the built-in eta-equality of Coq since version 8.5. This has been tested with 8.5pl2.

Update for Coq 8.8

LNMItPred.v (Version 2.10)
LNMItImp.v (Version 2.6.1)
LNGMItPred.v (Version 1.8)
LNGMItImp.v (Version 1.4)
LamFlatPred.v (Version 1.4)
README.txt
a TAR file with these six files and a partly useful _CoqProject file

All tested with Coq 8.8.2 (October 2018). The files LNMItPred.v, LNGMItPred.v, LamFlatPred.v now use bullet notation systematically, which is the most important change.

Ralph Matthes