package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.kernel/Names/index.html

Module NamesSource

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
Sourcemodule Id : sig ... end

Representation and operations on identifiers.

Sourcemodule Name : sig ... end

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

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

Sourcemodule Cset : CSig.SetS with type elt = Constant.t
Sourcemodule Cset_env : CSig.SetS with type elt = Constant.t
Sourcemodule Cmap : Util.Map.ExtS 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.

Sourcemodule Cmap_env : Util.Map.ExtS 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
Sourcemodule MutInd : sig ... end
Sourcemodule Mindset : CSig.SetS with type elt = MutInd.t
Sourcemodule Mindmap : Util.Map.ExtS with type key = MutInd.t and module Set := Mindset
Sourcemodule Ind : sig ... end
Sourcetype inductive = Ind.t
Sourcemodule Construct : sig ... end
Sourcetype constructor = Construct.t
Sourcemodule Indset : CSet.S with type elt = inductive
Sourcemodule Constrset : CSet.S with type elt = constructor
Sourcemodule Indset_env : CSet.S with type elt = inductive
Sourcemodule Indmap : CMap.ExtS with type key = inductive and module Set := Indset
Sourcemodule Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset
Sourcemodule Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env
Sourcemodule Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env
Sourceval ind_modpath : inductive -> ModPath.t
  • deprecated Use the Ind module
Sourceval constr_modpath : constructor -> ModPath.t
  • deprecated Use the Construct module
Sourceval ith_mutual_inductive : inductive -> int -> inductive
Sourceval ith_constructor_of_inductive : inductive -> int -> constructor
Sourceval inductive_of_constructor : constructor -> inductive
Sourceval index_of_constructor : constructor -> int
Sourceval eq_ind : inductive -> inductive -> bool
  • deprecated Use the Ind module
Sourceval eq_user_ind : inductive -> inductive -> bool
  • deprecated Use the Ind module
Sourceval eq_syntactic_ind : inductive -> inductive -> bool
  • deprecated Use the Ind module
Sourceval ind_ord : inductive -> inductive -> int
  • deprecated Use the Ind module
Sourceval ind_hash : inductive -> int
  • deprecated Use the Ind module
Sourceval ind_user_ord : inductive -> inductive -> int
  • deprecated Use the Ind module
Sourceval ind_user_hash : inductive -> int
  • deprecated Use the Ind module
Sourceval ind_syntactic_ord : inductive -> inductive -> int
  • deprecated Use the Ind module
Sourceval ind_syntactic_hash : inductive -> int
  • deprecated Use the Ind module
Sourceval eq_constructor : constructor -> constructor -> bool
  • deprecated Use the Construct module
Sourceval eq_user_constructor : constructor -> constructor -> bool
  • deprecated Use the Construct module
Sourceval eq_syntactic_constructor : constructor -> constructor -> bool
  • deprecated Use the Construct module
Sourceval constructor_ord : constructor -> constructor -> int
  • deprecated Use the Construct module
Sourceval constructor_hash : constructor -> int
  • deprecated Use the Construct module
Sourceval constructor_user_ord : constructor -> constructor -> int
  • deprecated Use the Construct module
Sourceval constructor_user_hash : constructor -> int
  • deprecated Use the Construct module
Sourceval constructor_syntactic_ord : constructor -> constructor -> int
  • deprecated Use the Construct module
Sourceval constructor_syntactic_hash : constructor -> int
  • deprecated Use the Construct module
Hash-consing
Sourceval hcons_con : Constant.t -> Constant.t
Sourceval hcons_mind : MutInd.t -> MutInd.t
Sourceval hcons_ind : inductive -> inductive
Sourceval hcons_construct : constructor -> constructor
Sourcetype 'a tableKey =
  1. | ConstKey of 'a
  2. | VarKey of Id.t
  3. | RelKey of Int.t
Sourcetype inv_rel_key = int

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

Sourceval eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
Sourceval eq_constant_key : Constant.t -> Constant.t -> bool

equalities on constant and inductive names (for the checker)

Sourceval eq_ind_chk : inductive -> inductive -> bool
Module paths
Sourcetype module_path = ModPath.t =
  1. | MPfile of DirPath.t
  2. | MPbound of MBId.t
  3. | MPdot of ModPath.t * Label.t
  • deprecated Alias type
Sourcemodule Projection : sig ... end
Global reference is a kernel side type for all references together
Sourcemodule GlobRef : sig ... end

Located identifiers and objects with syntax.

Sourcetype lident = Id.t CAst.t
Sourcetype lname = Name.t CAst.t
Sourcetype lstring = string CAst.t
Sourceval 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