|
<h1>The Core Library</h1>
<p>Here is a short description of the core 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 core library is composed of the following subdirectories:</p>
<dl>
<dt id="Init"> <a href="#Init"><b>Init</b></a>:
The prelude (automatically loaded when starting Coq)
</dt>
<dd>
theories/Corelib/Init/Ltac.v
theories/Corelib/Init/Notations.v
theories/Corelib/Init/Datatypes.v
theories/Corelib/Init/Logic.v
theories/Corelib/Init/Byte.v
theories/Corelib/Init/Nat.v
theories/Corelib/Init/Decimal.v
theories/Corelib/Init/Hexadecimal.v
theories/Corelib/Init/Number.v
theories/Corelib/Init/Peano.v
theories/Corelib/Init/Specif.v
theories/Corelib/Init/Sumbool.v
theories/Corelib/Init/Tactics.v
theories/Corelib/Init/Tauto.v
theories/Corelib/Init/Wf.v
(theories/Corelib/Init/Prelude.v)
</dd>
<dt id="Binary-numbers"> <a href="#Binary-numbers">Binary numbers</b></a>:
Basic definitions of binary arithmetic
</dt>
<dd>
theories/Corelib/Numbers/BinNums.v
theories/Corelib/BinNums/PosDef.v
theories/Corelib/BinNums/NatDef.v
theories/Corelib/BinNums/IntDef.v
</dd>
<dt id="Cyclic"> <a href="#Cyclic"><b>Cyclic</b></a>:
63-bits-based cyclic arithmetic
</dt>
<dd>
theories/Corelib/Numbers/Cyclic/Int63/CarryType.v
theories/Corelib/Numbers/Cyclic/Int63/PrimInt63.v
theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v
theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v
</dd>
<dt id="Floats"> <a href="#Floats"><b>Floats</b></a>:
Floating-point arithmetic
</dt>
<dd>
theories/Corelib/Floats/FloatClass.v
theories/Corelib/Floats/PrimFloat.v
theories/Corelib/Floats/SpecFloat.v
theories/Corelib/Floats/FloatOps.v
theories/Corelib/Floats/FloatAxioms.v
</dd>
<dt id="Relations"> <a href="#Relations"><b>Relations</b></a>:
Relations (definitions)
</dt>
<dd>
theories/Corelib/Relations/Relation_Definitions.v
</dd>
<dt id="Classes"> <a href="#Classes"><b>Classes</b></a>:
</dt>
<dd>
theories/Corelib/Classes/Init.v
theories/Corelib/Classes/RelationClasses.v
theories/Corelib/Classes/Morphisms.v
theories/Corelib/Classes/Morphisms_Prop.v
theories/Corelib/Classes/Equivalence.v
theories/Corelib/Classes/CRelationClasses.v
theories/Corelib/Classes/CMorphisms.v
theories/Corelib/Classes/SetoidTactics.v
</dd>
<dt id="Setoids"> <a href="#Setoids"><b>Setoids</b></a>:
</dt>
<dd>
theories/Corelib/Setoids/Setoid.v
</dd>
<dt id="Lists"> <a href="#Lists"><b>Lists</b></a>:
Polymorphic lists
</dt>
<dd>
theories/Corelib/Lists/ListDef.v
</dd>
<dt id="Program"> <a href="#Program"><b>Program</b></a>:
Support for dependently-typed programming
</dt>
<dd>
theories/Corelib/Program/Basics.v
theories/Corelib/Program/Wf.v
theories/Corelib/Program/Tactics.v
theories/Corelib/Program/Utils.v
</dd>
<dt id="SSReflect"> <a href="#SSReflect"><b>SSReflect</b></a>:
Base libraries for the SSReflect proof language and the
small scale reflection formalization technique
</dt>
<dd>
theories/Corelib/ssrmatching/ssrmatching.v
theories/Corelib/ssr/ssrclasses.v
theories/Corelib/ssr/ssreflect.v
theories/Corelib/ssr/ssrbool.v
theories/Corelib/ssr/ssrfun.v
</dd>
<dt id="Ltac2"> <a href="#Ltac2"><b>Ltac2</b></a>:
The Ltac2 tactic programming language
</dt>
<dd>
theories/Ltac2/Ltac2.v
theories/Ltac2/Array.v
theories/Ltac2/Bool.v
theories/Ltac2/Char.v
theories/Ltac2/Constant.v
theories/Ltac2/Constr.v
theories/Ltac2/Constructor.v
theories/Ltac2/Control.v
theories/Ltac2/Env.v
theories/Ltac2/Evar.v
theories/Ltac2/Float.v
theories/Ltac2/FMap.v
theories/Ltac2/FSet.v
theories/Ltac2/Fresh.v
theories/Ltac2/Ident.v
theories/Ltac2/Ind.v
theories/Ltac2/Init.v
theories/Ltac2/Int.v
theories/Ltac2/Lazy.v
theories/Ltac2/List.v
theories/Ltac2/Ltac1.v
theories/Ltac2/Ltac1CompatNotations.v
theories/Ltac2/Message.v
theories/Ltac2/Meta.v
theories/Ltac2/Notations.v
theories/Ltac2/Option.v
theories/Ltac2/Pattern.v
theories/Ltac2/Printf.v
theories/Ltac2/Proj.v
theories/Ltac2/Pstring.v
theories/Ltac2/RedFlags.v
theories/Ltac2/Ref.v
theories/Ltac2/Rewrite.v
theories/Ltac2/Std.v
theories/Ltac2/String.v
theories/Ltac2/TransparentState.v
theories/Ltac2/Uint63.v
theories/Ltac2/Unification.v
</dd>
<dt id="Compat"> <a href="#Compat"><b>Compat</b></a>:
Compatibility wrappers for previous versions of Coq
</dt>
<dd>
theories/Corelib/Compat/Coq818.v
theories/Corelib/Compat/Coq819.v
theories/Corelib/Compat/Coq820.v
theories/Corelib/Compat/Rocq90.v
theories/Ltac2/Compat/Coq818.v
theories/Ltac2/Compat/Coq819.v
</dd>
<dt id="Array"> <a href="#Array"><b>Array</b></a>:
Persistent native arrays
</dt>
<dd>
theories/Corelib/Array/PrimArray.v
theories/Corelib/Array/ArrayAxioms.v
</dd>
<dt id="Primitive-strings"> <a href="#Primitive-strings"><b>Primitive strings</b></a>:
Native string type
</dt>
<dd>
theories/Corelib/Strings/PrimString.v
theories/Corelib/Strings/PrimStringAxioms.v
</dd>
</dl>
[ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
]
|
