package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

This file defines a lot of different notions of names used pervasively in the kernel as well as in other places. The essential datatypes exported by this API are:

  • Id.t is the type of identifiers, that is morally a subset of strings which only contains Unicode characters of the Letter kind (and a few more).
  • Name.t is an ad-hoc variant of Id.t option allowing to handle optionally named objects.
  • DirPath.t represents generic paths as sequences of identifiers.
  • Label.t is an equivalent of Id.t made distinct for semantical purposes.
  • ModPath.t are module paths.
  • KerName.t are absolute names of objects in Coq.
Identifiers
module Id : sig ... end

Representation and operations on identifiers.

module Name : sig ... end

Representation and operations on identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax).

Type aliases
type name = Name.t =
  1. | Anonymous
  2. | Name of Id.t
  • deprecated Use Name.t
type variable = Id.t
type module_ident = Id.t
module ModIdset : Util.Set.S with type elt = module_ident
module ModIdmap : Util.Map.ExtS with type key = module_ident and module Set := ModIdset
Directory paths = section names paths
module DirPath : sig ... end
module DPset : Util.Set.S with type elt = DirPath.t
module DPmap : Util.Map.ExtS with type key = DirPath.t and module Set := DPset
Names of structure elements
module Label : sig ... end
Unique names for bound modules
module MBId : sig ... end
module MBIset : Util.Set.S with type elt = MBId.t
module MBImap : Util.Map.ExtS with type key = MBId.t and module Set := MBIset
The module part of the kernel name
module ModPath : sig ... end
module MPset : Util.Set.S with type elt = ModPath.t
module MPmap : Util.Map.ExtS with type key = ModPath.t and module Set := MPset
The absolute names of objects seen by kernel
module KerName : sig ... end
module KNset : CSig.USetS with type elt = KerName.t
module KNpred : Predicate.S with type elt = KerName.t
module KNmap : Util.Map.UExtS with type key = KerName.t and module Set := KNset
Signature for quotiented names
module type EqType = sig ... end
module type QNameS = sig ... end
Constant Names
module Constant : sig ... end
module Cpred : Predicate.S with type elt = Constant.t

The *_env modules consider an order on user part of names the others consider an order on canonical part of names

module Cset : CSig.USetS with type elt = Constant.t
module Cset_env : CSig.USetS with type elt = Constant.t
module Cmap : Util.Map.UExtS with type key = Constant.t and module Set := Cset

A map whose keys are constants (values of the Constant.t type). Keys are ordered wrt. "canonical form" of the constant.

module Cmap_env : Util.Map.UExtS with type key = Constant.t and module Set := Cset_env

A map whose keys are constants (values of the Constant.t type). Keys are ordered wrt. "user form" of the constant.

Inductive names
module MutInd : sig ... end
module Mindset : CSig.USetS with type elt = MutInd.t
module Mindmap : Util.Map.UExtS with type key = MutInd.t and module Set := Mindset
module Mindmap_env : CMap.UExtS with type key = MutInd.t
module Ind : sig ... end
type inductive = Ind.t
module Construct : sig ... end
type constructor = Construct.t
module Indset : CSet.S with type elt = inductive
module Constrset : CSet.S with type elt = constructor
module Indset_env : CSet.S with type elt = inductive
module Constrset_env : CSet.S with type elt = constructor
module Indmap : CMap.ExtS with type key = inductive and module Set := Indset
module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset
module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env
module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
Hash-consing
val hcons_con : Constant.t -> Constant.t
val hcons_mind : MutInd.t -> MutInd.t
val hcons_ind : inductive -> inductive
val hcons_construct : constructor -> constructor
type 'a tableKey =
  1. | ConstKey of 'a
  2. | VarKey of Id.t
  3. | RelKey of Int.t
type inv_rel_key = int

index in the rel_context part of environment starting by the end, inverse of de Bruijn indice

val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
val hash_table_key : ('a -> int) -> 'a tableKey -> int
val eq_constant_key : Constant.t -> Constant.t -> bool

equalities on constant and inductive names (for the checker)

val eq_ind_chk : inductive -> inductive -> bool
Module paths
type module_path = ModPath.t =
  1. | MPfile of DirPath.t
  2. | MPbound of MBId.t
  3. | MPdot of ModPath.t * Label.t
  • deprecated Alias type
module Projection : sig ... end
module PRset : CSig.USetS with type elt = Projection.Repr.t
module PRmap : Util.Map.UExtS with type key = Projection.Repr.t and module Set := PRset

Predicate on projection representation (ignoring unfolding state)

Global reference is a kernel side type for all references together
module GlobRef : sig ... end

Located identifiers and objects with syntax.

type lident = Id.t CAst.t
type lname = Name.t CAst.t
type lstring = string CAst.t
val lident_eq : lident -> lident -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct