TLC is an alternative to the standard Coq library. The motivation for developing TLC is to take advantage of non-constructivism, extensionality and type-classes for obtaining simpler definitions and simpler proofs.

TLC includes a tactic library that provides enhanced versions for a large number of Coq tactics. These tactics help build proof scripts that are more robust and much more concise.

TLC includes the optimal fixed point combinator, which can be used for building arbitrarily-complex recursive and co-recursive definitions.

Note that, to a large extent, TLC can be used in conjunction with the standard library.