Coq files

You can find here the Coq development supporting the ITP submission on implicative algebras. Definitions and propositions in PDF directly point to the corresponding files, but you can directly browse the source files here. The whole development can be downloaded here.

This development compiles under Coq 8.7 with Charguéraud TLC library. Coq can be installed through opam (which is probably itself in your favorite distribution repositories):

opam init -n -j 2 # 2 is the number of CPU cores
opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq.8.7 && opam pin add coq 8.7

You might be wanting to install coqide too:

opam install coqide

The TLC library can be installed through the following procedure:

git clone https://gitlab.inria.fr/charguer/tlc.git
cd tlc
make
make install

To compile the files, a simple call to the Makefile (make) should do the job. Then you can browse any of the file with CoqIDE or you favorite IDE.