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.

The old MPC'08 development is here.

Update for Coq 8.4

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

Update for Coq 8.5

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

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