README.md 1.93 KB
Newer Older
charguer's avatar
charguer committed
1
# The TLC Coq library
charguer's avatar
charguer committed
2

charguer's avatar
charguer committed
3 4 5
Description
===========

POTTIER Francois's avatar
POTTIER Francois committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
TLC is a general-purpose library that provides an alternative to Coq's standard library.

   - TLC relies on the axioms of
     functional extensionality,
     propositional extensionality,
     and indefinite description (also known as Hilbert's epsilon operator).
     The consequences of these axioms include
     the law of the excluded middle
     as well as proof irrelevance.
     Accepting these axioms often makes life significantly simpler.
   - TLC takes advantage of Coq's type class mechanism.
     In particular, this allows for common operators and lemma names
     for all container data structures and all order relations.
   - TLC includes the optimal fixed point combinator,
     which allows arbitrarily-complex recursive and co-recursive definitions.
   - TLC provides a collection of tactics that enhance the default tactics
     provided by Coq. These tactics help construct more concise and more
     robust proof scripts.
charguer's avatar
charguer committed
24 25 26

Status:

charguer's avatar
charguer committed
27 28
   - The master branch compiles with both Coq 8.8 and Coq 8.9.
     There is also a branch for Coq 8.10.
charguer's avatar
charguer committed
29 30 31 32 33

Compatibility:

   - Disclaimer: to allow improving the design of TLC, backward compatibility is not guaranteed.
   - TLC should not be incompatible with use of the standard library.
POTTIER Francois's avatar
POTTIER Francois committed
34

35 36
Compilation
===========
charguer's avatar
charguer committed
37

38
The released versions of TLC are available via `opam`:
charguer's avatar
charguer committed
39

40 41
    opam repo add coq-released http://coq.inria.fr/opam/released
    opam install -j4 coq-tlc
charguer's avatar
charguer committed
42

POTTIER Francois's avatar
POTTIER Francois committed
43
A working copy of TLC can also be compiled and installed as follows:
charguer's avatar
charguer committed
44

45
    # first clone this repository, then descend into it, and:
POTTIER Francois's avatar
POTTIER Francois committed
46
    make -j4
47
    make install
charguer's avatar
charguer committed
48 49

Documentation
charguer's avatar
charguer committed
50
=============
charguer's avatar
charguer committed
51

52
Some (partial) documentation can be found in the directory [doc](doc/).
charguer's avatar
charguer committed
53

54 55
License
=======
charguer's avatar
charguer committed
56

57
All files in TLC are distributed under the GNU-LGPL license.
charguer's avatar
charguer committed
58

59
If you need a more permissive license, please contact the author.
charguer's avatar
charguer committed
60

61 62
Authors: Arthur Charguéraud,
with contributions from Armaël Guéneau and François Pottier.