Home

Awesome

Paco: Coq library for Parametric Coinduction

Build Status License

Paco is a Coq library for parametric coinduction. For more information, please see:

Paco also supports upto techniques using "companion". See:

Minki Cho refactored the implementation to speed up the compilation time.

The current version is v4.1.2, and it's compatible with Coq 8.13 - 8.15.

Installation

# from opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-paco

# from source
cd src; make; make install          # for library files
cd webpage; make                    # for documentation

Examples

See /src/examples.v and /src/tutorial.v for examples.