# The Coq Standard Library

Here is a short description of the Coq standard library, which is distributed with the system. It provides a set of modules directly available through the Require Import command.

The standard library is composed of the following subdirectories:

Init: The core library (automatically loaded when starting Coq)
Notations Datatypes Logic Logic_Type Peano Specif Tactics Wf (Prelude)
Logic: Classical logic and dependent equality
Classical_Pred_Set Classical_Pred_Type Classical_Prop Classical_Type (Classical) ClassicalFacts Decidable DecidableType DecidableTypeEx Eqdep_dec EqdepFacts Eqdep JMeq ChoiceFacts RelationalChoice ClassicalChoice ClassicalDescription ClassicalEpsilon ClassicalUniqueChoice Berardi Diaconescu Hurkens ProofIrrelevance ProofIrrelevanceFacts
Arith: Basic Peano arithmetic
Le Lt Plus Minus Mult Gt Between Peano_dec Compare_dec (Arith) Min Max Compare Div2 Div EqNat Euclid Even Bool_nat Factorial Wf_nat
NArith: Binary positive integers
BinPos BinNat (NArith) Pnat Nnat Ndigits Ndist Ndec .
ZArith: Binary integers
BinInt Zorder Zcompare Znat Zmin Zmax Zminmax Zabs Zeven auxiliary ZArith_dec Zbool Zmisc Wf_Z Zhints (ZArith_base) Zcomplements Zsqrt Zpower Zdiv Zlogarithm (ZArith) Zwf Zbinary Znumtheory Int
QArith: Rational numbers
QArith_base Qreduction Qring (QArith) Qreals Qcanon
Reals: Formalization of real numbers
Rdefinitions Raxioms RIneq DiscrR (Rbase) RList Ranalysis Rbasic_fun Rderiv Rfunctions Rgeom R_Ifp Rlimit Rseries Rsigma R_sqr Rtrigo_fun Rtrigo SplitAbsolu SplitRmult Alembert AltSeries ArithProp Binomial Cauchy_prod Cos_plus Cos_rel Exp_prop Integration MVT NewtonInt PSeries_reg PartSum R_sqrt Ranalysis1 Ranalysis2 Ranalysis3 Ranalysis4 Rcomplete RiemannInt RiemannInt_SF Rpower Rprod Rsqrt_def Rtopology Rtrigo_alt Rtrigo_calc Rtrigo_def Rtrigo_reg SeqProp SeqSeries Sqrt_reg (Reals)
Sets: Sets (classical, constructive, finite, infinite, powerset, etc.)
Classical_sets Constructive_sets Cpo Ensembles Finite_sets_facts Finite_sets Image Infinite_sets Integers Multiset Partial_Order Permut Powerset_Classical_facts Powerset_facts Powerset Relations_1_facts Relations_1 Relations_2_facts Relations_2 Relations_3_facts Relations_3 Uniset
Relations: Relations (definitions and basic results)
Relation_Definitions Relation_Operators Relations Operators_Properties Rstar Newman
Wellfounded: Well-founded Relations
Disjoint_Union Inclusion Inverse_Image Lexicographic_Exponentiation Lexicographic_Product Transitive_Closure Union Wellfounded Well_Ordering
Setoids:
Setoid
Bool: Booleans (basic functions and results)
Bool BoolEq DecBool IfProp Sumbool Zerob Bvector
Lists: Polymorphic lists, Streams (infinite sequences)
List ListSet MonoList SetoidList Streams TheoryList
FSets: Modular implementation of finite sets/maps using lists
OrderedType OrderedTypeAlt OrderedTypeEx FSetInterface FSetBridge FSetProperties FSetEqProperties FSetList (FSets) FSetFacts FSetAVL FSetToFiniteSet FSetWeakProperties FSetWeakInterface FSetWeakFacts FSetWeakList FSetWeak FMapInterface FMapList FMapPositive FMapIntMap FMapFacts (FMaps) FMapAVL FMapWeakInterface FMapWeakList FMapWeak FMapWeakFacts
IntMap: An implementation of finite sets/maps as trees indexed by addresses
Adalloc Map Fset Mapaxioms Mapiter Mapcanon Mapsubset Lsort Mapfold Mapcard Mapc Maplists Allmaps
Strings Implementation of string as list of ascii characters
Ascii String
Sorting: Axiomatizations of sorts
Heap Permutation Sorting PermutEq PermutSetoid
 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (7984 entries) Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (401 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (5228 entries) Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (292 entries) Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (184 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1519 entries) Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (85 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (275 entries)