package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. ...
  2. ...
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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.library/Libnames/index.html

Module LibnamesSource

Sourceval dirpath_of_string : string -> Names.DirPath.t

Dirpaths

Pop the suffix of a DirPath.t. Raises a Failure for an empty path

Sourceval pop_dirpath_n : int -> Names.DirPath.t -> Names.DirPath.t

Pop the suffix n times

Immediate prefix and basename of a DirPath.t. May raise Failure

Sourceval add_dirpath_suffix : Names.DirPath.t -> Names.Id.t -> Names.DirPath.t
Sourceval drop_dirpath_prefix : Names.DirPath.t -> Names.DirPath.t -> Names.DirPath.t
Sourceval is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
Sourceval is_dirpath_suffix_of : Names.DirPath.t -> Names.DirPath.t -> bool
Sourcetype full_path

Full paths are absolute paths of declarations

Sourceval eq_full_path : full_path -> full_path -> bool
Sourceval compare_full_path : full_path -> full_path -> int

Constructors of full_path

Sourceval add_path_suffix : full_path -> Names.Id.t -> full_path
Sourceval append_path : full_path -> Names.DirPath.t -> full_path

Destructors of full_path

Sourceval path_pop_n_suffixes : int -> full_path -> full_path

path_pop_n_suffixes n p removes the last n elements of p. Raises Failure if p is not long enough.

Sourceval path_pop_suffix : full_path -> full_path

path_pop_suffix p is path_pop_n_suffixes 1 p.

The prefix of the path

  • deprecated Compose [dirpath_of_path] and [pop_dirpath]
Sourceval basename : full_path -> Names.Id.t
Sourceval dirpath_of_path : full_path -> Names.DirPath.t

The full path as a DirPath.t.

Sourceval is_path_prefix_of : full_path -> Names.DirPath.t -> bool
Sourceval path_of_string : string -> full_path

Parsing and printing of section path as "root.module.id"

Sourceval string_of_path : full_path -> string
Sourceval pr_path : full_path -> Pp.t
Sourcemodule Spmap : CSig.MapS with type key = full_path
...

A qualid is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial qualifications of absolute names, including single identifiers. The qualid are used to access the name table.

Sourcetype qualid_r
Sourcetype qualid = qualid_r CAst.t
Sourceval make_qualid : ?loc:Loc.t -> Names.DirPath.t -> Names.Id.t -> qualid
Sourceval repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
Sourceval qualid_eq : qualid -> qualid -> bool
Sourceval is_qualid_suffix_of_full_path : qualid -> full_path -> bool
Sourceval pr_qualid : qualid -> Pp.t
Sourceval string_of_qualid : qualid -> string
Sourceval qualid_of_string : ?loc:Loc.t -> string -> qualid

Turns an absolute name, a dirpath, or an Id.t into a qualified name denoting the same name

Sourceval qualid_of_path : ?loc:Loc.t -> full_path -> qualid
Sourceval qualid_of_dirpath : ?loc:Loc.t -> Names.DirPath.t -> qualid
Sourceval qualid_of_ident : ?loc:Loc.t -> Names.Id.t -> qualid
Sourceval qualid_of_lident : Names.lident -> qualid
Sourceval qualid_is_ident : qualid -> bool
Sourceval qualid_path : qualid -> Names.DirPath.t
Sourceval qualid_basename : qualid -> Names.Id.t
Sourceval idset_mem_qualid : qualid -> Names.Id.Set.t -> bool

false when the qualid is not an ident

...
Sourceval rocq_init_root : Names.Id.t

This is the root of the rocq-core library

Sourceval rocq_init_string : string
Sourceval default_root_prefix : Names.DirPath.t

This is the default root prefix for developments which doesn't mention a root

Sourceval dummy_full_path : full_path

For uninitialized data, cf DirPath.dummy