README.md 1.97 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:

POTTIER Francois's avatar
POTTIER Francois committed
27
   - The current version of TLC works with Coq 8.6 and 8.7.
charguer's avatar
charguer committed
28
   - TLC 2.0 (beta) was released in November 2017, with a complete polishing phase.
POTTIER Francois's avatar
POTTIER Francois committed
29

charguer's avatar
charguer committed
30 31 32 33 34

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
35

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

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

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

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

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

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

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

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

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

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

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