diff options
Diffstat (limited to 'doc/stdlib/index-list.html.template')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 626 |
1 files changed, 626 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template new file mode 100644 index 0000000000..a561de1d0c --- /dev/null +++ b/doc/stdlib/index-list.html.template @@ -0,0 +1,626 @@ + +<h1>The Coq Standard Library</h1> + +<p>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 <tt>Require Import</tt> command.</p> + +<p>The standard library is composed of the following subdirectories:</p> + +<dl> + <dt> <b>Init</b>: + The core library (automatically loaded when starting Coq) + </dt> + <dd> + theories/Init/Notations.v + theories/Init/Datatypes.v + theories/Init/Logic.v + theories/Init/Logic_Type.v + theories/Init/Byte.v + theories/Init/Nat.v + theories/Init/Decimal.v + theories/Init/Peano.v + theories/Init/Specif.v + theories/Init/Tactics.v + theories/Init/Tauto.v + theories/Init/Wf.v + (theories/Init/Prelude.v) + </dd> + + <dt> <b>Logic</b>: + Classical logic, dependent equality, extensionality, choice axioms + </dt> + <dd> + theories/Logic/SetIsType.v + theories/Logic/StrictProp.v + theories/Logic/Classical_Pred_Type.v + theories/Logic/Classical_Prop.v + (theories/Logic/Classical.v) + theories/Logic/ClassicalFacts.v + theories/Logic/Decidable.v + theories/Logic/Eqdep_dec.v + theories/Logic/EqdepFacts.v + theories/Logic/Eqdep.v + theories/Logic/JMeq.v + theories/Logic/ChoiceFacts.v + theories/Logic/RelationalChoice.v + theories/Logic/ClassicalChoice.v + theories/Logic/ClassicalDescription.v + theories/Logic/ClassicalEpsilon.v + theories/Logic/ClassicalUniqueChoice.v + theories/Logic/SetoidChoice.v + theories/Logic/Berardi.v + theories/Logic/Diaconescu.v + theories/Logic/Hurkens.v + theories/Logic/ProofIrrelevance.v + theories/Logic/ProofIrrelevanceFacts.v + theories/Logic/ConstructiveEpsilon.v + theories/Logic/Description.v + theories/Logic/Epsilon.v + theories/Logic/IndefiniteDescription.v + theories/Logic/PropExtensionality.v + theories/Logic/PropExtensionalityFacts.v + theories/Logic/FunctionalExtensionality.v + theories/Logic/ExtensionalFunctionRepresentative.v + theories/Logic/ExtensionalityFacts.v + theories/Logic/WeakFan.v + theories/Logic/WKL.v + theories/Logic/FinFun.v + theories/Logic/PropFacts.v + </dd> + + <dt> <b>Structures</b>: + Algebraic structures (types with equality, with order, ...). + DecidableType* and OrderedType* are there only for compatibility. + </dt> + <dd> + theories/Structures/Equalities.v + theories/Structures/EqualitiesFacts.v + theories/Structures/Orders.v + theories/Structures/OrdersTac.v + theories/Structures/OrdersAlt.v + theories/Structures/OrdersEx.v + theories/Structures/OrdersFacts.v + theories/Structures/OrdersLists.v + theories/Structures/GenericMinMax.v + theories/Structures/DecidableType.v + theories/Structures/DecidableTypeEx.v + theories/Structures/OrderedType.v + theories/Structures/OrderedTypeAlt.v + theories/Structures/OrderedTypeEx.v + </dd> + + <dt> <b>Bool</b>: + Booleans (basic functions and results) + </dt> + <dd> + theories/Bool/Bool.v + theories/Bool/BoolEq.v + theories/Bool/DecBool.v + theories/Bool/IfProp.v + theories/Bool/Sumbool.v + theories/Bool/Zerob.v + theories/Bool/Bvector.v + </dd> + + <dt> <b>Arith</b>: + Basic Peano arithmetic + </dt> + <dd> + theories/Arith/PeanoNat.v + theories/Arith/Le.v + theories/Arith/Lt.v + theories/Arith/Plus.v + theories/Arith/Minus.v + theories/Arith/Mult.v + theories/Arith/Gt.v + theories/Arith/Between.v + theories/Arith/Peano_dec.v + theories/Arith/Compare_dec.v + (theories/Arith/Arith_base.v) + (theories/Arith/Arith.v) + theories/Arith/Min.v + theories/Arith/Max.v + theories/Arith/Compare.v + theories/Arith/Div2.v + theories/Arith/EqNat.v + theories/Arith/Euclid.v + theories/Arith/Even.v + theories/Arith/Bool_nat.v + theories/Arith/Factorial.v + theories/Arith/Wf_nat.v + </dd> + + <dt> <b>PArith</b>: + Binary positive integers + </dt> + <dd> + theories/PArith/BinPosDef.v + theories/PArith/BinPos.v + theories/PArith/Pnat.v + theories/PArith/POrderedType.v + (theories/PArith/PArith.v) + </dd> + + <dt> <b>NArith</b>: + Binary natural numbers + </dt> + <dd> + theories/NArith/BinNatDef.v + theories/NArith/BinNat.v + theories/NArith/Nnat.v + theories/NArith/Ndigits.v + theories/NArith/Ndist.v + theories/NArith/Ndec.v + theories/NArith/Ndiv_def.v + theories/NArith/Ngcd_def.v + theories/NArith/Nsqrt_def.v + (theories/NArith/NArith.v) + </dd> + + <dt> <b>ZArith</b>: + Binary integers + </dt> + <dd> + theories/ZArith/BinIntDef.v + theories/ZArith/BinInt.v + theories/ZArith/Zorder.v + theories/ZArith/Zcompare.v + theories/ZArith/Znat.v + theories/ZArith/Zmin.v + theories/ZArith/Zmax.v + theories/ZArith/Zminmax.v + theories/ZArith/Zabs.v + theories/ZArith/Zeven.v + theories/ZArith/auxiliary.v + theories/ZArith/ZArith_dec.v + theories/ZArith/Zbool.v + theories/ZArith/Zmisc.v + theories/ZArith/Wf_Z.v + theories/ZArith/Zhints.v + (theories/ZArith/ZArith_base.v) + theories/ZArith/Zcomplements.v + theories/ZArith/Zsqrt_compat.v + theories/ZArith/Zpow_def.v + theories/ZArith/Zpow_alt.v + theories/ZArith/Zpower.v + theories/ZArith/Zdiv.v + theories/ZArith/Zquot.v + theories/ZArith/Zeuclid.v + theories/ZArith/Zlogarithm.v + (theories/ZArith/ZArith.v) + theories/ZArith/Zgcd_alt.v + theories/ZArith/Zwf.v + theories/ZArith/Znumtheory.v + theories/ZArith/Int.v + theories/ZArith/Zpow_facts.v + theories/ZArith/Zdigits.v + </dd> + + <dt> <b>QArith</b>: + Rational numbers + </dt> + <dd> + theories/QArith/QArith_base.v + theories/QArith/Qabs.v + theories/QArith/Qpower.v + theories/QArith/Qreduction.v + theories/QArith/Qring.v + theories/QArith/Qfield.v + (theories/QArith/QArith.v) + theories/QArith/Qreals.v + theories/QArith/Qcanon.v + theories/QArith/Qcabs.v + theories/QArith/Qround.v + theories/QArith/QOrderedType.v + theories/QArith/Qminmax.v + </dd> + + <dt> <b>Numbers</b>: + An experimental modular architecture for arithmetic + </dt> + <dd> + <dl> + <dt> <b> Prelude</b>: + </dt> + <dd> + theories/Numbers/BinNums.v + theories/Numbers/NumPrelude.v + theories/Numbers/NaryFunctions.v + theories/Numbers/AltBinNotations.v + theories/Numbers/DecimalFacts.v + theories/Numbers/DecimalNat.v + theories/Numbers/DecimalPos.v + theories/Numbers/DecimalN.v + theories/Numbers/DecimalZ.v + theories/Numbers/DecimalString.v + </dd> + + <dt> <b> NatInt</b>: + Abstract mixed natural/integer/cyclic arithmetic + </dt> + <dd> + theories/Numbers/NatInt/NZAdd.v + theories/Numbers/NatInt/NZAddOrder.v + theories/Numbers/NatInt/NZAxioms.v + theories/Numbers/NatInt/NZBase.v + theories/Numbers/NatInt/NZMul.v + theories/Numbers/NatInt/NZDiv.v + theories/Numbers/NatInt/NZMulOrder.v + theories/Numbers/NatInt/NZOrder.v + theories/Numbers/NatInt/NZDomain.v + theories/Numbers/NatInt/NZProperties.v + theories/Numbers/NatInt/NZParity.v + theories/Numbers/NatInt/NZPow.v + theories/Numbers/NatInt/NZSqrt.v + theories/Numbers/NatInt/NZLog.v + theories/Numbers/NatInt/NZGcd.v + theories/Numbers/NatInt/NZBits.v + </dd> + + <dt> <b> Cyclic</b>: + Abstract and 63-bits-based cyclic arithmetic + </dt> + <dd> + theories/Numbers/Cyclic/Abstract/CyclicAxioms.v + theories/Numbers/Cyclic/Abstract/NZCyclic.v + theories/Numbers/Cyclic/Abstract/DoubleType.v + theories/Numbers/Cyclic/Int31/Cyclic31.v + theories/Numbers/Cyclic/Int31/Ring31.v + theories/Numbers/Cyclic/Int31/Int31.v + theories/Numbers/Cyclic/Int63/Cyclic63.v + theories/Numbers/Cyclic/Int63/Int63.v + theories/Numbers/Cyclic/Int63/Ring63.v + theories/Numbers/Cyclic/ZModulo/ZModulo.v + </dd> + + <dt> <b> Natural</b>: + Abstract and 63-bits-words-based natural arithmetic + </dt> + <dd> + theories/Numbers/Natural/Abstract/NAdd.v + theories/Numbers/Natural/Abstract/NAddOrder.v + theories/Numbers/Natural/Abstract/NAxioms.v + theories/Numbers/Natural/Abstract/NBase.v + theories/Numbers/Natural/Abstract/NDefOps.v + theories/Numbers/Natural/Abstract/NIso.v + theories/Numbers/Natural/Abstract/NMulOrder.v + theories/Numbers/Natural/Abstract/NOrder.v + theories/Numbers/Natural/Abstract/NStrongRec.v + theories/Numbers/Natural/Abstract/NSub.v + theories/Numbers/Natural/Abstract/NDiv.v + theories/Numbers/Natural/Abstract/NMaxMin.v + theories/Numbers/Natural/Abstract/NParity.v + theories/Numbers/Natural/Abstract/NPow.v + theories/Numbers/Natural/Abstract/NSqrt.v + theories/Numbers/Natural/Abstract/NLog.v + theories/Numbers/Natural/Abstract/NGcd.v + theories/Numbers/Natural/Abstract/NLcm.v + theories/Numbers/Natural/Abstract/NBits.v + theories/Numbers/Natural/Abstract/NProperties.v + theories/Numbers/Natural/Binary/NBinary.v + theories/Numbers/Natural/Peano/NPeano.v + </dd> + + <dt> <b> Integer</b>: + Abstract and concrete (especially 63-bits-words-based) integer + arithmetic + </dt> + <dd> + theories/Numbers/Integer/Abstract/ZAdd.v + theories/Numbers/Integer/Abstract/ZAddOrder.v + theories/Numbers/Integer/Abstract/ZAxioms.v + theories/Numbers/Integer/Abstract/ZBase.v + theories/Numbers/Integer/Abstract/ZLt.v + theories/Numbers/Integer/Abstract/ZMul.v + theories/Numbers/Integer/Abstract/ZMulOrder.v + theories/Numbers/Integer/Abstract/ZSgnAbs.v + theories/Numbers/Integer/Abstract/ZMaxMin.v + theories/Numbers/Integer/Abstract/ZParity.v + theories/Numbers/Integer/Abstract/ZPow.v + theories/Numbers/Integer/Abstract/ZGcd.v + theories/Numbers/Integer/Abstract/ZLcm.v + theories/Numbers/Integer/Abstract/ZBits.v + theories/Numbers/Integer/Abstract/ZProperties.v + theories/Numbers/Integer/Abstract/ZDivEucl.v + theories/Numbers/Integer/Abstract/ZDivFloor.v + theories/Numbers/Integer/Abstract/ZDivTrunc.v + theories/Numbers/Integer/Binary/ZBinary.v + theories/Numbers/Integer/NatPairs/ZNatPairs.v + </dd> + </dl> + </dd> + + <dt> <b>Relations</b>: + Relations (definitions and basic results) + </dt> + <dd> + theories/Relations/Relation_Definitions.v + theories/Relations/Relation_Operators.v + theories/Relations/Relations.v + theories/Relations/Operators_Properties.v + </dd> + + <dt> <b>Sets</b>: + Sets (classical, constructive, finite, infinite, powerset, etc.) + </dt> + <dd> + theories/Sets/Classical_sets.v + theories/Sets/Constructive_sets.v + theories/Sets/Cpo.v + theories/Sets/Ensembles.v + theories/Sets/Finite_sets_facts.v + theories/Sets/Finite_sets.v + theories/Sets/Image.v + theories/Sets/Infinite_sets.v + theories/Sets/Integers.v + theories/Sets/Multiset.v + theories/Sets/Partial_Order.v + theories/Sets/Permut.v + theories/Sets/Powerset_Classical_facts.v + theories/Sets/Powerset_facts.v + theories/Sets/Powerset.v + theories/Sets/Relations_1_facts.v + theories/Sets/Relations_1.v + theories/Sets/Relations_2_facts.v + theories/Sets/Relations_2.v + theories/Sets/Relations_3_facts.v + theories/Sets/Relations_3.v + theories/Sets/Uniset.v + </dd> + + <dt> <b>Classes</b>: + </dt> + <dd> + theories/Classes/Init.v + theories/Classes/RelationClasses.v + theories/Classes/Morphisms.v + theories/Classes/Morphisms_Prop.v + theories/Classes/Morphisms_Relations.v + theories/Classes/Equivalence.v + theories/Classes/CRelationClasses.v + theories/Classes/CMorphisms.v + theories/Classes/CEquivalence.v + theories/Classes/EquivDec.v + theories/Classes/SetoidTactics.v + theories/Classes/SetoidClass.v + theories/Classes/SetoidDec.v + theories/Classes/RelationPairs.v + theories/Classes/DecidableClass.v + </dd> + + <dt> <b>Setoids</b>: + </dt> + <dd> + theories/Setoids/Setoid.v + </dd> + + <dt> <b>Lists</b>: + Polymorphic lists, Streams (infinite sequences) + </dt> + <dd> + theories/Lists/List.v + theories/Lists/ListDec.v + theories/Lists/ListSet.v + theories/Lists/SetoidList.v + theories/Lists/SetoidPermutation.v + theories/Lists/Streams.v + theories/Lists/StreamMemo.v + theories/Lists/ListTactics.v + </dd> + + <dt> <b>Vectors</b>: + Dependent datastructures storing their length + </dt> + <dd> + theories/Vectors/Fin.v + theories/Vectors/VectorDef.v + theories/Vectors/VectorSpec.v + theories/Vectors/VectorEq.v + (theories/Vectors/Vector.v) + </dd> + + <dt> <b>Sorting</b>: + Axiomatizations of sorts + </dt> + <dd> + theories/Sorting/Heap.v + theories/Sorting/Permutation.v + theories/Sorting/Sorting.v + theories/Sorting/PermutEq.v + theories/Sorting/PermutSetoid.v + theories/Sorting/Mergesort.v + theories/Sorting/Sorted.v + </dd> + + <dt> <b>Wellfounded</b>: + Well-founded Relations + </dt> + <dd> + theories/Wellfounded/Disjoint_Union.v + theories/Wellfounded/Inclusion.v + theories/Wellfounded/Inverse_Image.v + theories/Wellfounded/Lexicographic_Exponentiation.v + theories/Wellfounded/Lexicographic_Product.v + theories/Wellfounded/Transitive_Closure.v + theories/Wellfounded/Union.v + theories/Wellfounded/Wellfounded.v + theories/Wellfounded/Well_Ordering.v + </dd> + + <dt> <b>MSets</b>: + Modular implementation of finite sets using lists or + efficient trees. This is a modernization of FSets. + </dt> + <dd> + theories/MSets/MSetInterface.v + theories/MSets/MSetFacts.v + theories/MSets/MSetDecide.v + theories/MSets/MSetProperties.v + theories/MSets/MSetEqProperties.v + theories/MSets/MSetWeakList.v + theories/MSets/MSetList.v + theories/MSets/MSetGenTree.v + theories/MSets/MSetAVL.v + theories/MSets/MSetRBT.v + theories/MSets/MSetPositive.v + theories/MSets/MSetToFiniteSet.v + (theories/MSets/MSets.v) + </dd> + + <dt> <b>FSets</b>: + Modular implementation of finite sets/maps using lists or + efficient trees. For sets, please consider the more + modern MSets. + </dt> + <dd> + theories/FSets/FSetInterface.v + theories/FSets/FSetBridge.v + theories/FSets/FSetFacts.v + theories/FSets/FSetDecide.v + theories/FSets/FSetProperties.v + theories/FSets/FSetEqProperties.v + theories/FSets/FSetList.v + theories/FSets/FSetWeakList.v + theories/FSets/FSetCompat.v + theories/FSets/FSetAVL.v + theories/FSets/FSetPositive.v + (theories/FSets/FSets.v) + theories/FSets/FSetToFiniteSet.v + theories/FSets/FMapInterface.v + theories/FSets/FMapWeakList.v + theories/FSets/FMapList.v + theories/FSets/FMapPositive.v + theories/FSets/FMapFacts.v + (theories/FSets/FMaps.v) + theories/FSets/FMapAVL.v + theories/FSets/FMapFullAVL.v + </dd> + + <dt> <b>Strings</b> + Implementation of string as list of ascii characters + </dt> + <dd> + theories/Strings/Byte.v + theories/Strings/Ascii.v + theories/Strings/String.v + theories/Strings/BinaryString.v + theories/Strings/HexString.v + theories/Strings/OctalString.v + theories/Strings/ByteVector.v + </dd> + + <dt> <b>Reals</b>: + Formalization of real numbers + </dt> + <dd> + theories/Reals/Rdefinitions.v + theories/Reals/Raxioms.v + theories/Reals/RIneq.v + theories/Reals/DiscrR.v + theories/Reals/ROrderedType.v + theories/Reals/Rminmax.v + (theories/Reals/Rbase.v) + theories/Reals/RList.v + theories/Reals/Ranalysis.v + theories/Reals/Rbasic_fun.v + theories/Reals/Rderiv.v + theories/Reals/Rfunctions.v + theories/Reals/Rgeom.v + theories/Reals/R_Ifp.v + theories/Reals/Rlimit.v + theories/Reals/Rseries.v + theories/Reals/Rsigma.v + theories/Reals/R_sqr.v + theories/Reals/Rtrigo_fun.v + theories/Reals/Rtrigo1.v + theories/Reals/Rtrigo.v + theories/Reals/Ratan.v + theories/Reals/Machin.v + theories/Reals/SplitAbsolu.v + theories/Reals/SplitRmult.v + theories/Reals/Alembert.v + theories/Reals/AltSeries.v + theories/Reals/ArithProp.v + theories/Reals/Binomial.v + theories/Reals/Cauchy_prod.v + theories/Reals/Cos_plus.v + theories/Reals/Cos_rel.v + theories/Reals/Exp_prop.v + theories/Reals/Integration.v + theories/Reals/MVT.v + theories/Reals/NewtonInt.v + theories/Reals/PSeries_reg.v + theories/Reals/PartSum.v + theories/Reals/R_sqrt.v + theories/Reals/Ranalysis1.v + theories/Reals/Ranalysis2.v + theories/Reals/Ranalysis3.v + theories/Reals/Ranalysis4.v + theories/Reals/Ranalysis5.v + theories/Reals/Ranalysis_reg.v + theories/Reals/Rcomplete.v + theories/Reals/RiemannInt.v + theories/Reals/RiemannInt_SF.v + theories/Reals/Rpow_def.v + theories/Reals/Rpower.v + theories/Reals/Rprod.v + theories/Reals/Rsqrt_def.v + theories/Reals/Rtopology.v + theories/Reals/Rtrigo_alt.v + theories/Reals/Rtrigo_calc.v + theories/Reals/Rtrigo_def.v + theories/Reals/Rtrigo_reg.v + theories/Reals/SeqProp.v + theories/Reals/SeqSeries.v + theories/Reals/Sqrt_reg.v + theories/Reals/Rlogic.v + (theories/Reals/Reals.v) + theories/Reals/Runcountable.v + </dd> + + <dt> <b>Program</b>: + Support for dependently-typed programming + </dt> + <dd> + theories/Program/Basics.v + theories/Program/Wf.v + theories/Program/Subset.v + theories/Program/Equality.v + theories/Program/Tactics.v + theories/Program/Utils.v + theories/Program/Syntax.v + theories/Program/Program.v + theories/Program/Combinators.v + </dd> + + <dt> <b>SSReflect</b>: + Base libraries for the SSReflect proof language and the + small scale reflection formalization technique + </dt> + <dd> + plugins/ssrmatching/ssrmatching.v + plugins/ssr/ssreflect.v + plugins/ssr/ssrbool.v + plugins/ssr/ssrfun.v + </dd> + + <dt> <b>Unicode</b>: + Unicode-based notations + </dt> + <dd> + theories/Unicode/Utf8_core.v + theories/Unicode/Utf8.v + </dd> + + <dt> <b>Compat</b>: + Compatibility wrappers for previous versions of Coq + </dt> + <dd> + theories/Compat/AdmitAxiom.v + theories/Compat/Coq88.v + theories/Compat/Coq89.v + theories/Compat/Coq810.v + </dd> +</dl> |