← Back to branch summary

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

« back to all changes in this revision

Viewing changes to doc/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:
doc/stdlib/index-list.html.template
 
1
 
 
2
<h1>The Coq Standard Library</h1>
 
3
 
 
4
<p>Here is a short description of the Coq standard library, which is
 
5
distributed with the system.
 
6
It provides a set of modules directly available 
 
7
through the <tt>Require Import</tt> command.</p>
 
8
 
 
9
<p>The standard library is composed of the following subdirectories:</p>
 
10
 
 
11
<dl>
 
12
  <dt> <b>Init</b>:
 
13
    The core library (automatically loaded when starting Coq)
 
14
  </dt>
 
15
  <dd> 
 
16
    theories/Init/Notations.v
 
17
    theories/Init/Datatypes.v
 
18
    theories/Init/Logic.v
 
19
    theories/Init/Logic_Type.v
 
20
    theories/Init/Peano.v
 
21
    theories/Init/Specif.v
 
22
    theories/Init/Tactics.v
 
23
    theories/Init/Wf.v
 
24
    (theories/Init/Prelude.v)
 
25
  </dd>
 
26
  
 
27
  <dt> <b>Logic</b>:
 
28
      Classical logic and dependent equality
 
29
  </dt>
 
30
  <dd>
 
31
    theories/Logic/SetIsType.v
 
32
    theories/Logic/Classical_Pred_Set.v
 
33
    theories/Logic/Classical_Pred_Type.v
 
34
    theories/Logic/Classical_Prop.v
 
35
    theories/Logic/Classical_Type.v
 
36
    (theories/Logic/Classical.v)
 
37
    theories/Logic/ClassicalFacts.v
 
38
    theories/Logic/Decidable.v
 
39
    theories/Logic/DecidableType.v
 
40
    theories/Logic/DecidableTypeEx.v
 
41
    theories/Logic/Eqdep_dec.v
 
42
    theories/Logic/EqdepFacts.v
 
43
    theories/Logic/Eqdep.v
 
44
    theories/Logic/JMeq.v
 
45
    theories/Logic/ChoiceFacts.v
 
46
    theories/Logic/RelationalChoice.v
 
47
    theories/Logic/ClassicalChoice.v
 
48
    theories/Logic/ClassicalDescription.v
 
49
    theories/Logic/ClassicalEpsilon.v
 
50
    theories/Logic/ClassicalUniqueChoice.v
 
51
    theories/Logic/Berardi.v
 
52
    theories/Logic/Diaconescu.v
 
53
    theories/Logic/Hurkens.v
 
54
    theories/Logic/ProofIrrelevance.v
 
55
    theories/Logic/ProofIrrelevanceFacts.v
 
56
    theories/Logic/ConstructiveEpsilon.v
 
57
    theories/Logic/Description.v
 
58
    theories/Logic/Epsilon.v
 
59
    theories/Logic/IndefiniteDescription.v
 
60
    theories/Logic/FunctionalExtensionality.v
 
61
  </dd>
 
62
    
 
63
  <dt> <b>Bool</b>:
 
64
       Booleans (basic functions and results)
 
65
  </dt>
 
66
  <dd> 
 
67
    theories/Bool/Bool.v
 
68
    theories/Bool/BoolEq.v
 
69
    theories/Bool/DecBool.v
 
70
    theories/Bool/IfProp.v
 
71
    theories/Bool/Sumbool.v
 
72
    theories/Bool/Zerob.v
 
73
    theories/Bool/Bvector.v
 
74
  </dd>
 
75
    
 
76
  <dt> <b>Arith</b>:
 
77
    Basic Peano arithmetic
 
78
  </dt>
 
79
  <dd> 
 
80
    theories/Arith/Arith_base.v
 
81
    theories/Arith/Le.v
 
82
    theories/Arith/Lt.v
 
83
    theories/Arith/Plus.v
 
84
    theories/Arith/Minus.v
 
85
    theories/Arith/Mult.v
 
86
    theories/Arith/Gt.v
 
87
    theories/Arith/Between.v
 
88
    theories/Arith/Peano_dec.v
 
89
    theories/Arith/Compare_dec.v
 
90
    (theories/Arith/Arith.v)
 
91
    theories/Arith/Min.v
 
92
    theories/Arith/Max.v
 
93
    theories/Arith/Compare.v
 
94
    theories/Arith/Div2.v
 
95
    theories/Arith/EqNat.v
 
96
    theories/Arith/Euclid.v
 
97
    theories/Arith/Even.v
 
98
    theories/Arith/Bool_nat.v
 
99
    theories/Arith/Factorial.v
 
100
    theories/Arith/Wf_nat.v
 
101
  </dd>
 
102
    
 
103
  <dt> <b>NArith</b>:
 
104
    Binary positive integers
 
105
  </dt>
 
106
  <dd> 
 
107
    theories/NArith/BinPos.v
 
108
    theories/NArith/BinNat.v
 
109
    (theories/NArith/NArith.v)
 
110
    theories/NArith/Pnat.v
 
111
    theories/NArith/Nnat.v
 
112
    theories/NArith/Ndigits.v
 
113
    theories/NArith/Ndist.v
 
114
    theories/NArith/Ndec.v
 
115
  </dd>
 
116
 
 
117
  <dt> <b>ZArith</b>:
 
118
       Binary integers
 
119
  </dt>
 
120
  <dd> 
 
121
    theories/ZArith/BinInt.v
 
122
    theories/ZArith/Zorder.v
 
123
    theories/ZArith/Zcompare.v
 
124
    theories/ZArith/Znat.v
 
125
    theories/ZArith/Zmin.v
 
126
    theories/ZArith/Zmax.v
 
127
    theories/ZArith/Zminmax.v
 
128
    theories/ZArith/Zabs.v
 
129
    theories/ZArith/Zeven.v
 
130
    theories/ZArith/auxiliary.v
 
131
    theories/ZArith/ZArith_dec.v
 
132
    theories/ZArith/Zbool.v
 
133
    theories/ZArith/Zmisc.v
 
134
    theories/ZArith/Wf_Z.v
 
135
    theories/ZArith/Zhints.v
 
136
    (theories/ZArith/ZArith_base.v)
 
137
    theories/ZArith/Zcomplements.v
 
138
    theories/ZArith/Zsqrt.v
 
139
    theories/ZArith/Zpow_def.v
 
140
    theories/ZArith/Zpower.v
 
141
    theories/ZArith/Zdiv.v
 
142
    theories/ZArith/Zlogarithm.v
 
143
    (theories/ZArith/ZArith.v)
 
144
    theories/ZArith/Zgcd_alt.v
 
145
    theories/ZArith/Zwf.v
 
146
    theories/ZArith/Zbinary.v
 
147
    theories/ZArith/Znumtheory.v
 
148
    theories/ZArith/Int.v
 
149
    theories/ZArith/ZOdiv_def.v
 
150
    theories/ZArith/ZOdiv.v
 
151
    theories/ZArith/Zpow_facts.v
 
152
  </dd>
 
153
 
 
154
  <dt> <b>QArith</b>:
 
155
    Rational numbers
 
156
  </dt>
 
157
  <dd>
 
158
    theories/QArith/QArith_base.v
 
159
    theories/QArith/Qabs.v
 
160
    theories/QArith/Qpower.v
 
161
    theories/QArith/Qreduction.v
 
162
    theories/QArith/Qring.v
 
163
    theories/QArith/Qfield.v
 
164
    (theories/QArith/QArith.v)
 
165
    theories/QArith/Qreals.v
 
166
    theories/QArith/Qcanon.v
 
167
    theories/QArith/Qround.v
 
168
  </dd>
 
169
 
 
170
  <dt> <b>Numbers</b>: 
 
171
    A modular axiomatic construction for numbers
 
172
  </dt>
 
173
  <dd>
 
174
  theories/Numbers/NumPrelude.v
 
175
  theories/Numbers/BigNumPrelude.v
 
176
  theories/Numbers/NaryFunctions.v
 
177
  </dd>
 
178
  
 
179
  <dd>
 
180
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
 
181
theories/Numbers/Cyclic/Abstract/NZCyclic.v
 
182
theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
 
183
theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
 
184
theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
 
185
theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
 
186
theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
 
187
theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
 
188
theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
 
189
theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
 
190
theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
 
191
theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
 
192
theories/Numbers/Cyclic/Int31/Cyclic31.v
 
193
theories/Numbers/Cyclic/Int31/Int31.v
 
194
theories/Numbers/Cyclic/ZModulo/ZModulo.v
 
195
  </dd>
 
196
 
 
197
  <dd>
 
198
    theories/Numbers/Integer/Abstract/ZAdd.v
 
199
theories/Numbers/Integer/Abstract/ZAddOrder.v
 
200
theories/Numbers/Integer/Abstract/ZAxioms.v
 
201
theories/Numbers/Integer/Abstract/ZBase.v
 
202
theories/Numbers/Integer/Abstract/ZDomain.v
 
203
theories/Numbers/Integer/Abstract/ZLt.v
 
204
theories/Numbers/Integer/Abstract/ZMul.v
 
205
theories/Numbers/Integer/Abstract/ZMulOrder.v
 
206
theories/Numbers/Integer/BigZ/BigZ.v
 
207
theories/Numbers/Integer/BigZ/ZMake.v
 
208
theories/Numbers/Integer/Binary/ZBinary.v
 
209
theories/Numbers/Integer/NatPairs/ZNatPairs.v
 
210
theories/Numbers/Integer/SpecViaZ/ZSig.v
 
211
theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
 
212
  </dd>
 
213
 
 
214
  <dd>
 
215
theories/Numbers/NatInt/NZAdd.v
 
216
theories/Numbers/NatInt/NZAddOrder.v
 
217
theories/Numbers/NatInt/NZAxioms.v
 
218
theories/Numbers/NatInt/NZBase.v
 
219
theories/Numbers/NatInt/NZMul.v
 
220
theories/Numbers/NatInt/NZMulOrder.v
 
221
theories/Numbers/NatInt/NZOrder.v
 
222
  </dd>
 
223
 
 
224
  <dd>
 
225
theories/Numbers/Natural/Abstract/NAdd.v
 
226
theories/Numbers/Natural/Abstract/NAddOrder.v
 
227
theories/Numbers/Natural/Abstract/NAxioms.v
 
228
theories/Numbers/Natural/Abstract/NBase.v
 
229
theories/Numbers/Natural/Abstract/NDefOps.v
 
230
theories/Numbers/Natural/Abstract/NIso.v
 
231
theories/Numbers/Natural/Abstract/NMul.v
 
232
theories/Numbers/Natural/Abstract/NMulOrder.v
 
233
theories/Numbers/Natural/Abstract/NOrder.v
 
234
theories/Numbers/Natural/Abstract/NStrongRec.v
 
235
theories/Numbers/Natural/Abstract/NSub.v
 
236
theories/Numbers/Natural/BigN/BigN.v
 
237
theories/Numbers/Natural/BigN/Nbasic.v
 
238
theories/Numbers/Natural/BigN/NMake.v
 
239
theories/Numbers/Natural/Binary/NBinary.v
 
240
theories/Numbers/Natural/Binary/NBinDefs.v
 
241
theories/Numbers/Natural/Peano/NPeano.v
 
242
theories/Numbers/Natural/SpecViaZ/NSig.v
 
243
theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
 
244
  </dd>
 
245
 
 
246
  <dd>
 
247
    theories/Numbers/Rational/BigQ/BigQ.v
 
248
    theories/Numbers/Rational/BigQ/QMake.v
 
249
    theories/Numbers/Rational/SpecViaQ/QSig.v
 
250
  </dd>
 
251
  
 
252
  <dt> <b>Relations</b>:
 
253
       Relations (definitions and basic results)
 
254
  </dt>
 
255
  <dd> 
 
256
    theories/Relations/Relation_Definitions.v
 
257
    theories/Relations/Relation_Operators.v
 
258
    theories/Relations/Relations.v
 
259
    theories/Relations/Operators_Properties.v
 
260
<!-- Deprecated 
 
261
    theories/Relations/Rstar.v
 
262
    theories/Relations/Newman.v
 
263
-->
 
264
  </dd>
 
265
    
 
266
  <dt> <b>Sets</b>:
 
267
       Sets (classical, constructive, finite, infinite, powerset, etc.)
 
268
  </dt>
 
269
  <dd> 
 
270
    theories/Sets/Classical_sets.v
 
271
    theories/Sets/Constructive_sets.v
 
272
    theories/Sets/Cpo.v
 
273
    theories/Sets/Ensembles.v
 
274
    theories/Sets/Finite_sets_facts.v
 
275
    theories/Sets/Finite_sets.v
 
276
    theories/Sets/Image.v
 
277
    theories/Sets/Infinite_sets.v
 
278
    theories/Sets/Integers.v
 
279
    theories/Sets/Multiset.v
 
280
    theories/Sets/Partial_Order.v
 
281
    theories/Sets/Permut.v
 
282
    theories/Sets/Powerset_Classical_facts.v
 
283
    theories/Sets/Powerset_facts.v
 
284
    theories/Sets/Powerset.v
 
285
    theories/Sets/Relations_1_facts.v
 
286
    theories/Sets/Relations_1.v
 
287
    theories/Sets/Relations_2_facts.v
 
288
    theories/Sets/Relations_2.v
 
289
    theories/Sets/Relations_3_facts.v
 
290
    theories/Sets/Relations_3.v
 
291
    theories/Sets/Uniset.v
 
292
  </dd>
 
293
    
 
294
  <dt> <b>Classes</b>:
 
295
  <dd> 
 
296
    theories/Classes/Init.v
 
297
    theories/Classes/RelationClasses.v
 
298
    theories/Classes/Morphisms.v
 
299
    theories/Classes/Morphisms_Prop.v
 
300
    theories/Classes/Morphisms_Relations.v
 
301
    theories/Classes/Equivalence.v
 
302
    theories/Classes/EquivDec.v
 
303
    theories/Classes/Functions.v
 
304
    theories/Classes/SetoidTactics.v
 
305
    theories/Classes/SetoidClass.v
 
306
    theories/Classes/SetoidDec.v
 
307
    theories/Classes/SetoidAxioms.v
 
308
  </dd>
 
309
 
 
310
  <dt> <b>Setoids</b>:
 
311
 
 
312
  <dd> 
 
313
    theories/Setoids/Setoid.v
 
314
  </dd>
 
315
    
 
316
  <dt> <b>Lists</b>:
 
317
    Polymorphic lists, Streams (infinite sequences)
 
318
  </dt>
 
319
  <dd> 
 
320
    theories/Lists/List.v
 
321
    theories/Lists/ListSet.v
 
322
    theories/Lists/MonoList.v
 
323
    theories/Lists/SetoidList.v
 
324
    theories/Lists/Streams.v
 
325
    theories/Lists/StreamMemo.v
 
326
    theories/Lists/TheoryList.v
 
327
    theories/Lists/ListTactics.v
 
328
  </dd>
 
329
 
 
330
  <dt> <b>Sorting</b>:
 
331
    Axiomatizations of sorts
 
332
  </dt>
 
333
  <dd> 
 
334
    theories/Sorting/Heap.v
 
335
    theories/Sorting/Permutation.v
 
336
    theories/Sorting/Sorting.v
 
337
    theories/Sorting/PermutEq.v
 
338
    theories/Sorting/PermutSetoid.v
 
339
  </dd>
 
340
 
 
341
  <dt> <b>Wellfounded</b>:
 
342
       Well-founded Relations
 
343
  </dt>
 
344
  <dd> 
 
345
    theories/Wellfounded/Disjoint_Union.v
 
346
    theories/Wellfounded/Inclusion.v
 
347
    theories/Wellfounded/Inverse_Image.v
 
348
    theories/Wellfounded/Lexicographic_Exponentiation.v
 
349
    theories/Wellfounded/Lexicographic_Product.v
 
350
    theories/Wellfounded/Transitive_Closure.v
 
351
    theories/Wellfounded/Union.v
 
352
    theories/Wellfounded/Wellfounded.v
 
353
    theories/Wellfounded/Well_Ordering.v
 
354
  </dd>
 
355
    
 
356
  <dt> <b>FSets</b>:
 
357
    Modular implementation of finite sets/maps using lists or
 
358
    efficient trees
 
359
  </dt>
 
360
  <dd>
 
361
    theories/FSets/OrderedType.v
 
362
    theories/FSets/OrderedTypeAlt.v
 
363
    theories/FSets/OrderedTypeEx.v
 
364
    theories/FSets/FSetInterface.v
 
365
    theories/FSets/FSetBridge.v
 
366
    theories/FSets/FSetFacts.v
 
367
    theories/FSets/FSetDecide.v
 
368
    theories/FSets/FSetProperties.v
 
369
    theories/FSets/FSetEqProperties.v
 
370
    theories/FSets/FSetList.v
 
371
    theories/FSets/FSetWeakList.v
 
372
    (theories/FSets/FSets.v)
 
373
    theories/FSets/FSetAVL.v
 
374
    theories/FSets/FSetToFiniteSet.v
 
375
    theories/FSets/FMapInterface.v
 
376
    theories/FSets/FMapWeakList.v
 
377
    theories/FSets/FMapList.v
 
378
    theories/FSets/FMapPositive.v
 
379
    theories/FSets/FMapFacts.v
 
380
    (theories/FSets/FMaps.v)
 
381
    theories/FSets/FMapAVL.v
 
382
    theories/FSets/FSetFullAVL.v
 
383
    theories/FSets/FMapFullAVL.v
 
384
  </dd>
 
385
 
 
386
<!--  <dt> <b>Strings</b>
 
387
    Implementation of string as list of ascii characters
 
388
  </dt>
 
389
  <dd>
 
390
    theories/Strings/Ascii.v
 
391
    theories/Strings/String.v
 
392
  </dd> -->
 
393
    
 
394
  <dt> <b>Reals</b>:
 
395
    Formalization of real numbers
 
396
  </dt>
 
397
  <dd> 
 
398
    theories/Reals/Rdefinitions.v
 
399
    theories/Reals/Raxioms.v
 
400
    theories/Reals/RIneq.v
 
401
    theories/Reals/DiscrR.v
 
402
    (theories/Reals/Rbase.v)
 
403
    theories/Reals/RList.v
 
404
    theories/Reals/Ranalysis.v
 
405
    theories/Reals/Rbasic_fun.v
 
406
    theories/Reals/Rderiv.v
 
407
    theories/Reals/Rfunctions.v
 
408
    theories/Reals/Rgeom.v
 
409
    theories/Reals/R_Ifp.v
 
410
    theories/Reals/Rlimit.v
 
411
    theories/Reals/Rseries.v
 
412
    theories/Reals/Rsigma.v
 
413
    theories/Reals/R_sqr.v
 
414
    theories/Reals/Rtrigo_fun.v
 
415
    theories/Reals/Rtrigo.v
 
416
    theories/Reals/SplitAbsolu.v
 
417
    theories/Reals/SplitRmult.v
 
418
    theories/Reals/Alembert.v
 
419
    theories/Reals/AltSeries.v
 
420
    theories/Reals/ArithProp.v
 
421
    theories/Reals/Binomial.v
 
422
    theories/Reals/Cauchy_prod.v
 
423
    theories/Reals/Cos_plus.v
 
424
    theories/Reals/Cos_rel.v
 
425
    theories/Reals/Exp_prop.v
 
426
    theories/Reals/Integration.v
 
427
    theories/Reals/MVT.v
 
428
    theories/Reals/NewtonInt.v
 
429
    theories/Reals/PSeries_reg.v
 
430
    theories/Reals/PartSum.v
 
431
    theories/Reals/R_sqrt.v
 
432
    theories/Reals/Ranalysis1.v
 
433
    theories/Reals/Ranalysis2.v
 
434
    theories/Reals/Ranalysis3.v
 
435
    theories/Reals/Ranalysis4.v
 
436
    theories/Reals/Rcomplete.v
 
437
    theories/Reals/RiemannInt.v
 
438
    theories/Reals/RiemannInt_SF.v
 
439
    theories/Reals/Rpow_def.v
 
440
    theories/Reals/Rpower.v
 
441
    theories/Reals/Rprod.v
 
442
    theories/Reals/Rsqrt_def.v
 
443
    theories/Reals/Rtopology.v
 
444
    theories/Reals/Rtrigo_alt.v
 
445
    theories/Reals/Rtrigo_calc.v
 
446
    theories/Reals/Rtrigo_def.v
 
447
    theories/Reals/Rtrigo_reg.v
 
448
    theories/Reals/SeqProp.v
 
449
    theories/Reals/SeqSeries.v
 
450
    theories/Reals/Sqrt_reg.v
 
451
    theories/Reals/Rlogic.v
 
452
    theories/Reals/LegacyRfield.v
 
453
    (theories/Reals/Reals.v)
 
454
  </dd>
 
455
    
 
456
  <dt> <b>Program</b>:
 
457
    Support for dependently-typed programming.
 
458
  </dt>
 
459
  <dd> 
 
460
    theories/Program/Basics.v
 
461
    theories/Program/Wf.v
 
462
    theories/Program/Subset.v
 
463
    theories/Program/Equality.v
 
464
    theories/Program/Tactics.v
 
465
    theories/Program/Utils.v
 
466
    theories/Program/Syntax.v
 
467
    theories/Program/Program.v
 
468
    theories/Program/Combinators.v
 
469
  </dd>
 
470
 
 
471
</dl>