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)

Ltac Notations Equality Datatypes Logic Byte Nat Decimal Hexadecimal Number Peano Specif Sumbool Tactics Tauto Wf (Prelude)

Binary numbers: Basic definitions of binary arithmetic

BinNums PosDef NatDef IntDef

Cyclic: 63-bits-based cyclic arithmetic

CarryType PrimInt63 Uint63Axioms Sint63Axioms

Floats: Floating-point arithmetic

FloatClass PrimFloat SpecFloat FloatOps FloatAxioms

Relations: Relations (definitions)

Relation_Definitions

Classes:

Init RelationClasses Morphisms Morphisms_Prop Equivalence CRelationClasses CMorphisms SetoidTactics

Setoids:

Setoid

Lists: Polymorphic lists

ListDef

Program: Support for dependently-typed programming

Basics Wf Tactics Utils

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

ssrmatching ssrclasses ssreflect_rw ssreflect ssrbool ssrfun

Ltac2: The Ltac2 tactic programming language

Ltac2 Array Bool Char Constant Constr Constructor Control Env Evar Float FMap FSet Fresh Ident Ind Init Int Lazy List Ltac1 Ltac1CompatNotations Message Meta Module Notations Option Pattern Printf Proj Pstring RedFlags Ref Reference Rewrite Scheme Std String TransparentState Uint63 Unification

Compat: Compatibility wrappers for previous versions of Coq

Coq818 Coq819 Coq820 Rocq90 Rocq91 Rocq92 Coq818 Coq819

Array: Persistent native arrays

PrimArray ArrayAxioms

Primitive strings: Native string type

PrimString PrimStringAxioms