package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.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
Sourcemodule Fresh : 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