summaryrefslogtreecommitdiff
path: root/doc/stdlib/index-list.html.template
diff options
context:
space:
mode:
Diffstat (limited to 'doc/stdlib/index-list.html.template')
-rw-r--r--doc/stdlib/index-list.html.template150
1 files changed, 88 insertions, 62 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index cbb8580d..10744fe4 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -41,16 +41,20 @@ through the <tt>Require Import</tt> command.</p>
theories/Logic/Classical_Prop.v
theories/Logic/Classical_Type.v
(theories/Logic/Classical.v)
+ theories/Logic/ClassicalFacts.v
theories/Logic/Decidable.v
+ theories/Logic/DecidableType.v
+ theories/Logic/DecidableTypeEx.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/ChoiceFacts.v
theories/Logic/ClassicalDescription.v
- theories/Logic/ClassicalFacts.v
+ theories/Logic/ClassicalEpsilon.v
+ theories/Logic/ClassicalUniqueChoice.v
theories/Logic/Berardi.v
theories/Logic/Diaconescu.v
theories/Logic/Hurkens.v
@@ -93,7 +97,11 @@ through the <tt>Require Import</tt> command.</p>
theories/NArith/BinNat.v
(theories/NArith/NArith.v)
theories/NArith/Pnat.v
- </dd>
+ theories/NArith/Nnat.v
+ theories/NArith/Ndigits.v
+ theories/NArith/Ndist.v
+ theories/NArith/Ndec.v
+. </dd>
<dt> <b>ZArith</b>:
Binary integers
@@ -124,6 +132,18 @@ through the <tt>Require Import</tt> command.</p>
theories/ZArith/Zwf.v
theories/ZArith/Zbinary.v
theories/ZArith/Znumtheory.v
+ theories/ZArith/Int.v
+ </dd>
+
+ <dt> <b>Reals</b>:
+ Rational numbers
+ </dt>
+ <dd>
+ theories/QArith/QArith_base.v
+ theories/QArith/Qreduction.v
+ theories/QArith/Qring.v
+ (theories/QArith/QArith.v)
+ theories/QArith/Qreals.v
</dd>
<dt> <b>Reals</b>:
@@ -185,32 +205,6 @@ through the <tt>Require Import</tt> command.</p>
(theories/Reals/Reals.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>Lists</b>:
- Polymorphic lists, Streams (infinite sequences)
- </dt>
- <dd>
- theories/Lists/List.v
- theories/Lists/ListSet.v
- theories/Lists/MonoList.v
- theories/Lists/MoreList.v
- theories/Lists/SetoidList.v
- theories/Lists/Streams.v
- theories/Lists/TheoryList.v
- </dd>
-
<dt> <b>Sets</b>:
Sets (classical, constructive, finite, infinite, powerset, etc.)
</dt>
@@ -266,67 +260,89 @@ through the <tt>Require Import</tt> command.</p>
theories/Wellfounded/Well_Ordering.v
</dd>
- <dt> <b>Sorting</b>:
- Axiomatizations of sorts
- </dt>
- <dd>
- theories/Sorting/Heap.v
- theories/Sorting/Permutation.v
- theories/Sorting/Sorting.v
- </dd>
-
<dt> <b>Setoids</b>:
<dd>
theories/Setoids/Setoid.v
</dd>
- <dt> <b>IntMap</b>:
- Finite sets/maps as trees indexed by addresses
+ <dt> <b>Bool</b>:
+ Booleans (basic functions and results)
</dt>
<dd>
- theories/IntMap/Addr.v
- theories/IntMap/Adist.v
- theories/IntMap/Addec.v
- theories/IntMap/Adalloc.v
- theories/IntMap/Map.v
- theories/IntMap/Fset.v
- theories/IntMap/Mapaxioms.v
- theories/IntMap/Mapiter.v
- theories/IntMap/Mapcanon.v
- theories/IntMap/Mapsubset.v
- theories/IntMap/Lsort.v
- theories/IntMap/Mapfold.v
- theories/IntMap/Mapcard.v
- theories/IntMap/Mapc.v
- theories/IntMap/Maplists.v
- theories/IntMap/Allmaps.v
+ 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>Lists</b>:
+ Polymorphic lists, Streams (infinite sequences)
+ </dt>
+ <dd>
+ theories/Lists/List.v
+ theories/Lists/ListSet.v
+ theories/Lists/MonoList.v
+ theories/Lists/SetoidList.v
+ theories/Lists/Streams.v
+ theories/Lists/TheoryList.v
+ </dd>
+
<dt> <b>FSets</b>:
Modular implementation of finite sets/maps using lists
</dt>
<dd>
- theories/FSets/DecidableType.v
theories/FSets/OrderedType.v
+ theories/FSets/OrderedTypeAlt.v
+ theories/FSets/OrderedTypeEx.v
theories/FSets/FSetInterface.v
theories/FSets/FSetBridge.v
theories/FSets/FSetProperties.v
theories/FSets/FSetEqProperties.v
- theories/FSets/FSetFacts.v
theories/FSets/FSetList.v
- theories/FSets/FSet.v
- theories/FSets/FMapInterface.v
- theories/FSets/FMapList.v
- theories/FSets/FMap.v
+ (theories/FSets/FSets.v)
+ theories/FSets/FSetFacts.v
+ theories/FSets/FSetAVL.v
+ theories/FSets/FSetToFiniteSet.v
+ theories/FSets/FSetWeakProperties.v
theories/FSets/FSetWeakInterface.v
theories/FSets/FSetWeakFacts.v
theories/FSets/FSetWeakList.v
theories/FSets/FSetWeak.v
+ theories/FSets/FMapInterface.v
+ theories/FSets/FMapList.v
+ theories/FSets/FMapPositive.v
+ theories/FSets/FMapIntMap.v
+ theories/FSets/FMapFacts.v
+ (theories/FSets/FMaps.v)
+ theories/FSets/FMapAVL.v
theories/FSets/FMapWeakInterface.v
theories/FSets/FMapWeakList.v
theories/FSets/FMapWeak.v
+ theories/FSets/FMapWeakFacts.v
</dd>
+ <dt> <b>IntMap</b>:
+ An implementation of finite sets/maps as trees indexed by addresses
+ </dt>
+ <dd>
+ theories/IntMap/Adalloc.v
+ theories/IntMap/Map.v
+ theories/IntMap/Fset.v
+ theories/IntMap/Mapaxioms.v
+ theories/IntMap/Mapiter.v
+ theories/IntMap/Mapcanon.v
+ theories/IntMap/Mapsubset.v
+ theories/IntMap/Lsort.v
+ theories/IntMap/Mapfold.v
+ theories/IntMap/Mapcard.v
+ theories/IntMap/Mapc.v
+ theories/IntMap/Maplists.v
+ theories/IntMap/Allmaps.v
+ </dd>
+
<dt> <b>Strings</b>
Implementation of string as list of ascii characters
</dt>
@@ -335,5 +351,15 @@ through the <tt>Require Import</tt> command.</p>
theories/Strings/String.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
</dd>
+
</dl>
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 09:46:56 +0000