Permutations in Coinductive Graph Representation

All the following code is additional material to the article of the same name by the authors.

• The twelve Coq vernacular files with the implementation, the Makefile, the instructions for installation and the list of correspondences
• EqImplIso.v
• NatSeg.v
• Tools.v
• Fin.v
• ListEq.v
• Ilist.v
• Extroduce.v
• IlistPerm.v
• EquivContejean.v
• Graphs.v
• GPerm.v
• IPPJustification.v
• Makefile
• INSTALL.txt
• README.pdf

Reference [16] in the paper: the final version published in the ECEASST.

A newer and more complete version of the code is available here. It should also be maintained for the future versions of Coq.