package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

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 `Nameops`Source

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

Sourceval pr_meta : Constr.metavariable -> Pp.t

Metavariables

Sourceval string_of_meta : Constr.metavariable -> string