package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.engine/Nameops/index.html

Module NameopsSource

Identifiers and names

Sourceval make_ident : string -> int option -> Names.Id.t
Sourceval repr_ident : Names.Id.t -> string * int option
Sourceval atompart_of_id : Names.Id.t -> string

remove trailing digits

Sourceval root_of_id : Names.Id.t -> Names.Id.t

remove trailing digits, ' and _

Sourceval add_suffix : Names.Id.t -> string -> Names.Id.t
Sourceval add_prefix : string -> Names.Id.t -> Names.Id.t

Below, by subscript we mean a suffix composed solely from (decimal) digits.

Sourcemodule Subscript : sig ... end
Sourceval has_subscript : Names.Id.t -> bool
Sourceval get_subscript : Names.Id.t -> Names.Id.t * Subscript.t

Split an identifier into a base name and a subscript.

Sourceval add_subscript : Names.Id.t -> Subscript.t -> Names.Id.t

Append the subscript to the identifier.

Sourceval increment_subscript : Names.Id.t -> Names.Id.t

Return the same identifier as the original one but whose subscript is incremented. If the original identifier does not have a suffix, 0 is appended to it.

Example mappings:

bar ↦ bar0

bar0 ↦ bar1

bar00 ↦ bar01

bar1 ↦ bar2

bar01 ↦ bar01

bar9 ↦ bar10

bar09 ↦ bar10

bar99 ↦ bar100

Sourceval forget_subscript : Names.Id.t -> Names.Id.t
Sourcemodule Name : sig ... end

Metavariables

Sourceval string_of_meta : Constr.metavariable -> string