The Core Library

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 Require Import command.

The core library is composed of the following subdirectories:

Init: The prelude (automatically loaded when starting Coq)

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)

Binary numbers: Basic definitions of binary arithmetic

theories/Corelib/Numbers/BinNums.v theories/Corelib/BinNums/PosDef.v theories/Corelib/BinNums/NatDef.v theories/Corelib/BinNums/IntDef.v

Cyclic: 63-bits-based cyclic arithmetic

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

Floats: Floating-point arithmetic

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

Relations: Relations (definitions)

theories/Corelib/Relations/Relation_Definitions.v

Classes:

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

Setoids:

theories/Corelib/Setoids/Setoid.v

Lists: Polymorphic lists

theories/Corelib/Lists/ListDef.v

Program: Support for dependently-typed programming

theories/Corelib/Program/Basics.v theories/Corelib/Program/Wf.v theories/Corelib/Program/Tactics.v theories/Corelib/Program/Utils.v

SSReflect: Base libraries for the SSReflect proof language and the small scale reflection formalization technique

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

Ltac2: The Ltac2 tactic programming language

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

Compat: Compatibility wrappers for previous versions of Coq

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

Array: Persistent native arrays

theories/Corelib/Array/PrimArray.v theories/Corelib/Array/ArrayAxioms.v

Primitive strings: Native string type

theories/Corelib/Strings/PrimString.v theories/Corelib/Strings/PrimStringAxioms.v