← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to stdlib/index-list.html.template

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
stdlib/index-list.html.template
1
 
<html>
2
 
 
3
 
<head>
4
 
<link rel="stylesheet" href="coqdoc.css" type="text/css">
5
 
<title>The Coq Standard Library
6
 
</head>
7
 
 
8
 
<body>
9
 
 
10
 
<H1>The Coq Standard Library</H1>
11
 
 
12
 
<p>Here is a short description of the Coq standard library, which is
13
 
distributed with the system.
14
 
It provides a set of modules directly available 
15
 
through the <tt>Require Import</tt> command.</p>
16
 
 
17
 
<p>The standard library is composed of the following subdirectories:</p>
18
 
 
19
 
<dl>
20
 
  <dt> <b>Init</b>:
21
 
    The core library (automatically loaded when starting Coq)
22
 
  </dt>
23
 
  <dd> 
24
 
    theories/Init/Notations.v
25
 
    theories/Init/Datatypes.v
26
 
    theories/Init/Logic.v
27
 
    theories/Init/Logic_Type.v
28
 
    theories/Init/Peano.v
29
 
    theories/Init/Specif.v
30
 
    theories/Init/Tactics.v
31
 
    theories/Init/Wf.v
32
 
    (theories/Init/Prelude.v)
33
 
  </dd>
34
 
  
35
 
  <dt> <b>Logic</b>:
36
 
      Classical logic and dependent equality
37
 
  </dt>
38
 
  <dd>
39
 
    theories/Logic/Classical_Pred_Set.v
40
 
    theories/Logic/Classical_Pred_Type.v
41
 
    theories/Logic/Classical_Prop.v
42
 
    theories/Logic/Classical_Type.v
43
 
    (theories/Logic/Classical.v)
44
 
    theories/Logic/ClassicalFacts.v
45
 
    theories/Logic/Decidable.v
46
 
    theories/Logic/DecidableType.v
47
 
    theories/Logic/DecidableTypeEx.v
48
 
    theories/Logic/Eqdep_dec.v
49
 
    theories/Logic/EqdepFacts.v
50
 
    theories/Logic/Eqdep.v
51
 
    theories/Logic/JMeq.v
52
 
    theories/Logic/ChoiceFacts.v
53
 
    theories/Logic/RelationalChoice.v
54
 
    theories/Logic/ClassicalChoice.v
55
 
    theories/Logic/ClassicalDescription.v
56
 
    theories/Logic/ClassicalEpsilon.v
57
 
    theories/Logic/ClassicalUniqueChoice.v
58
 
    theories/Logic/Berardi.v
59
 
    theories/Logic/Diaconescu.v
60
 
    theories/Logic/Hurkens.v
61
 
    theories/Logic/ProofIrrelevance.v
62
 
    theories/Logic/ProofIrrelevanceFacts.v
63
 
  </dd>
64
 
    
65
 
  <dt> <b>Arith</b>:
66
 
    Basic Peano arithmetic
67
 
  </dt>
68
 
  <dd> 
69
 
    theories/Arith/Le.v
70
 
    theories/Arith/Lt.v
71
 
    theories/Arith/Plus.v
72
 
    theories/Arith/Minus.v
73
 
    theories/Arith/Mult.v
74
 
    theories/Arith/Gt.v
75
 
    theories/Arith/Between.v
76
 
    theories/Arith/Peano_dec.v
77
 
    theories/Arith/Compare_dec.v
78
 
    (theories/Arith/Arith.v)
79
 
    theories/Arith/Min.v
80
 
    theories/Arith/Max.v
81
 
    theories/Arith/Compare.v
82
 
    theories/Arith/Div2.v
83
 
    theories/Arith/Div.v
84
 
    theories/Arith/EqNat.v
85
 
    theories/Arith/Euclid.v
86
 
    theories/Arith/Even.v
87
 
    theories/Arith/Bool_nat.v
88
 
    theories/Arith/Factorial.v
89
 
    theories/Arith/Wf_nat.v
90
 
  </dd>
91
 
    
92
 
  <dt> <b>NArith</b>:
93
 
    Binary positive integers
94
 
  </dt>
95
 
  <dd> 
96
 
    theories/NArith/BinPos.v
97
 
    theories/NArith/BinNat.v
98
 
    (theories/NArith/NArith.v)
99
 
    theories/NArith/Pnat.v
100
 
    theories/NArith/Nnat.v
101
 
    theories/NArith/Ndigits.v
102
 
    theories/NArith/Ndist.v
103
 
    theories/NArith/Ndec.v
104
 
.  </dd>
105
 
 
106
 
  <dt> <b>ZArith</b>:
107
 
       Binary integers
108
 
  </dt>
109
 
  <dd> 
110
 
    theories/ZArith/BinInt.v
111
 
    theories/ZArith/Zorder.v
112
 
    theories/ZArith/Zcompare.v
113
 
    theories/ZArith/Znat.v
114
 
    theories/ZArith/Zmin.v
115
 
    theories/ZArith/Zmax.v
116
 
    theories/ZArith/Zminmax.v
117
 
    theories/ZArith/Zabs.v
118
 
    theories/ZArith/Zeven.v
119
 
    theories/ZArith/auxiliary.v
120
 
    theories/ZArith/ZArith_dec.v
121
 
    theories/ZArith/Zbool.v
122
 
    theories/ZArith/Zmisc.v
123
 
    theories/ZArith/Wf_Z.v
124
 
    theories/ZArith/Zhints.v
125
 
    (theories/ZArith/ZArith_base.v)
126
 
    theories/ZArith/Zcomplements.v
127
 
    theories/ZArith/Zsqrt.v
128
 
    theories/ZArith/Zpower.v
129
 
    theories/ZArith/Zdiv.v
130
 
    theories/ZArith/Zlogarithm.v
131
 
    (theories/ZArith/ZArith.v)
132
 
    theories/ZArith/Zwf.v
133
 
    theories/ZArith/Zbinary.v
134
 
    theories/ZArith/Znumtheory.v
135
 
    theories/ZArith/Int.v
136
 
  </dd>
137
 
 
138
 
  <dt> <b>QArith</b>:
139
 
    Rational numbers
140
 
  </dt>
141
 
  <dd>
142
 
    theories/QArith/QArith_base.v
143
 
    theories/QArith/Qreduction.v
144
 
    theories/QArith/Qring.v
145
 
    (theories/QArith/QArith.v)
146
 
    theories/QArith/Qreals.v
147
 
    theories/QArith/Qcanon.v
148
 
  </dd>
149
 
    
150
 
  <dt> <b>Reals</b>:
151
 
    Formalization of real numbers
152
 
  </dt>
153
 
  <dd> 
154
 
    theories/Reals/Rdefinitions.v
155
 
    theories/Reals/Raxioms.v
156
 
    theories/Reals/RIneq.v
157
 
    theories/Reals/DiscrR.v
158
 
    (theories/Reals/Rbase.v)
159
 
    theories/Reals/RList.v
160
 
    theories/Reals/Ranalysis.v
161
 
    theories/Reals/Rbasic_fun.v
162
 
    theories/Reals/Rderiv.v
163
 
    theories/Reals/Rfunctions.v
164
 
    theories/Reals/Rgeom.v
165
 
    theories/Reals/R_Ifp.v
166
 
    theories/Reals/Rlimit.v
167
 
    theories/Reals/Rseries.v
168
 
    theories/Reals/Rsigma.v
169
 
    theories/Reals/R_sqr.v
170
 
    theories/Reals/Rtrigo_fun.v
171
 
    theories/Reals/Rtrigo.v
172
 
    theories/Reals/SplitAbsolu.v
173
 
    theories/Reals/SplitRmult.v
174
 
    theories/Reals/Alembert.v
175
 
    theories/Reals/AltSeries.v
176
 
    theories/Reals/ArithProp.v
177
 
    theories/Reals/Binomial.v
178
 
    theories/Reals/Cauchy_prod.v
179
 
    theories/Reals/Cos_plus.v
180
 
    theories/Reals/Cos_rel.v
181
 
    theories/Reals/Exp_prop.v
182
 
    theories/Reals/Integration.v
183
 
    theories/Reals/MVT.v
184
 
    theories/Reals/NewtonInt.v
185
 
    theories/Reals/PSeries_reg.v
186
 
    theories/Reals/PartSum.v
187
 
    theories/Reals/R_sqrt.v
188
 
    theories/Reals/Ranalysis1.v
189
 
    theories/Reals/Ranalysis2.v
190
 
    theories/Reals/Ranalysis3.v
191
 
    theories/Reals/Ranalysis4.v
192
 
    theories/Reals/Rcomplete.v
193
 
    theories/Reals/RiemannInt.v
194
 
    theories/Reals/RiemannInt_SF.v
195
 
    theories/Reals/Rpower.v
196
 
    theories/Reals/Rprod.v
197
 
    theories/Reals/Rsqrt_def.v
198
 
    theories/Reals/Rtopology.v
199
 
    theories/Reals/Rtrigo_alt.v
200
 
    theories/Reals/Rtrigo_calc.v
201
 
    theories/Reals/Rtrigo_def.v
202
 
    theories/Reals/Rtrigo_reg.v
203
 
    theories/Reals/SeqProp.v
204
 
    theories/Reals/SeqSeries.v
205
 
    theories/Reals/Sqrt_reg.v
206
 
    (theories/Reals/Reals.v)
207
 
  </dd>
208
 
    
209
 
  <dt> <b>Sets</b>:
210
 
       Sets (classical, constructive, finite, infinite, powerset, etc.)
211
 
  </dt>
212
 
  <dd> 
213
 
    theories/Sets/Classical_sets.v
214
 
    theories/Sets/Constructive_sets.v
215
 
    theories/Sets/Cpo.v
216
 
    theories/Sets/Ensembles.v
217
 
    theories/Sets/Finite_sets_facts.v
218
 
    theories/Sets/Finite_sets.v
219
 
    theories/Sets/Image.v
220
 
    theories/Sets/Infinite_sets.v
221
 
    theories/Sets/Integers.v
222
 
    theories/Sets/Multiset.v
223
 
    theories/Sets/Partial_Order.v
224
 
    theories/Sets/Permut.v
225
 
    theories/Sets/Powerset_Classical_facts.v
226
 
    theories/Sets/Powerset_facts.v
227
 
    theories/Sets/Powerset.v
228
 
    theories/Sets/Relations_1_facts.v
229
 
    theories/Sets/Relations_1.v
230
 
    theories/Sets/Relations_2_facts.v
231
 
    theories/Sets/Relations_2.v
232
 
    theories/Sets/Relations_3_facts.v
233
 
    theories/Sets/Relations_3.v
234
 
    theories/Sets/Uniset.v
235
 
  </dd>
236
 
    
237
 
  <dt> <b>Relations</b>:
238
 
       Relations (definitions and basic results)
239
 
  </dt>
240
 
  <dd> 
241
 
    theories/Relations/Relation_Definitions.v
242
 
    theories/Relations/Relation_Operators.v
243
 
    theories/Relations/Relations.v
244
 
    theories/Relations/Operators_Properties.v
245
 
    theories/Relations/Rstar.v
246
 
    theories/Relations/Newman.v
247
 
  </dd>
248
 
    
249
 
  <dt> <b>Wellfounded</b>:
250
 
       Well-founded Relations
251
 
  </dt>
252
 
  <dd> 
253
 
    theories/Wellfounded/Disjoint_Union.v
254
 
    theories/Wellfounded/Inclusion.v
255
 
    theories/Wellfounded/Inverse_Image.v
256
 
    theories/Wellfounded/Lexicographic_Exponentiation.v
257
 
    theories/Wellfounded/Lexicographic_Product.v
258
 
    theories/Wellfounded/Transitive_Closure.v
259
 
    theories/Wellfounded/Union.v
260
 
    theories/Wellfounded/Wellfounded.v
261
 
    theories/Wellfounded/Well_Ordering.v
262
 
  </dd>
263
 
    
264
 
  <dt> <b>Setoids</b>:
265
 
  <dd> 
266
 
    theories/Setoids/Setoid.v
267
 
  </dd>
268
 
    
269
 
  <dt> <b>Bool</b>:
270
 
       Booleans (basic functions and results)
271
 
  </dt>
272
 
  <dd> 
273
 
    theories/Bool/Bool.v
274
 
    theories/Bool/BoolEq.v
275
 
    theories/Bool/DecBool.v
276
 
    theories/Bool/IfProp.v
277
 
    theories/Bool/Sumbool.v
278
 
    theories/Bool/Zerob.v
279
 
    theories/Bool/Bvector.v
280
 
  </dd>
281
 
    
282
 
  <dt> <b>Lists</b>:
283
 
    Polymorphic lists, Streams (infinite sequences)
284
 
  </dt>
285
 
  <dd> 
286
 
    theories/Lists/List.v
287
 
    theories/Lists/ListSet.v
288
 
    theories/Lists/MonoList.v
289
 
    theories/Lists/SetoidList.v
290
 
    theories/Lists/Streams.v
291
 
    theories/Lists/TheoryList.v
292
 
  </dd>
293
 
 
294
 
  <dt> <b>FSets</b>:
295
 
    Modular implementation of finite sets/maps using lists
296
 
  </dt>
297
 
  <dd>
298
 
    theories/FSets/OrderedType.v
299
 
    theories/FSets/OrderedTypeAlt.v
300
 
    theories/FSets/OrderedTypeEx.v
301
 
    theories/FSets/FSetInterface.v
302
 
    theories/FSets/FSetBridge.v
303
 
    theories/FSets/FSetProperties.v
304
 
    theories/FSets/FSetEqProperties.v
305
 
    theories/FSets/FSetList.v
306
 
    (theories/FSets/FSets.v)
307
 
    theories/FSets/FSetFacts.v
308
 
    theories/FSets/FSetAVL.v
309
 
    theories/FSets/FSetToFiniteSet.v
310
 
    theories/FSets/FSetWeakProperties.v
311
 
    theories/FSets/FSetWeakInterface.v
312
 
    theories/FSets/FSetWeakFacts.v
313
 
    theories/FSets/FSetWeakList.v
314
 
    theories/FSets/FSetWeak.v
315
 
    theories/FSets/FMapInterface.v
316
 
    theories/FSets/FMapList.v
317
 
    theories/FSets/FMapPositive.v
318
 
    theories/FSets/FMapIntMap.v
319
 
    theories/FSets/FMapFacts.v
320
 
    (theories/FSets/FMaps.v)
321
 
    theories/FSets/FMapAVL.v
322
 
    theories/FSets/FMapWeakInterface.v
323
 
    theories/FSets/FMapWeakList.v
324
 
    theories/FSets/FMapWeak.v
325
 
    theories/FSets/FMapWeakFacts.v
326
 
  </dd>
327
 
 
328
 
  <dt> <b>IntMap</b>:
329
 
    An implementation of finite sets/maps as trees indexed by addresses
330
 
  </dt>
331
 
  <dd> 
332
 
    theories/IntMap/Adalloc.v
333
 
    theories/IntMap/Map.v
334
 
    theories/IntMap/Fset.v
335
 
    theories/IntMap/Mapaxioms.v
336
 
    theories/IntMap/Mapiter.v
337
 
    theories/IntMap/Mapcanon.v
338
 
    theories/IntMap/Mapsubset.v
339
 
    theories/IntMap/Lsort.v
340
 
    theories/IntMap/Mapfold.v
341
 
    theories/IntMap/Mapcard.v
342
 
    theories/IntMap/Mapc.v
343
 
    theories/IntMap/Maplists.v
344
 
    theories/IntMap/Allmaps.v
345
 
  </dd>
346
 
    
347
 
  <dt> <b>Strings</b>
348
 
    Implementation of string as list of ascii characters
349
 
  </dt>
350
 
  <dd>
351
 
    theories/Strings/Ascii.v
352
 
    theories/Strings/String.v
353
 
  </dd>
354
 
    
355
 
  <dt> <b>Sorting</b>:
356
 
    Axiomatizations of sorts
357
 
  </dt>
358
 
  <dd> 
359
 
    theories/Sorting/Heap.v
360
 
    theories/Sorting/Permutation.v
361
 
    theories/Sorting/Sorting.v
362
 
    theories/Sorting/PermutEq.v
363
 
    theories/Sorting/PermutSetoid.v
364
 
  </dd>
365
 
 
366
 
</dl>