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 (4)

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.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

doc/rocq-runtime.kernel/Section/index.html

Module SectionSource

Kernel implementation of sections.

Sourcetype 'a t

Type of sections with additional data 'a

Sourceval depth : 'a t -> int

Number of nested sections.

Sourceval map_custom : ('a -> 'a) -> 'a t -> 'a t

Modify the custom data

Manipulating sections
Sourcetype section_entry =
  1. | SecDefinition of Names.Constant.t
  2. | SecInductive of Names.MutInd.t
Sourceval open_section : custom:'a -> 'a t option -> 'a t

Open a new section with the provided universe polymorphic status. Sections can be nested, with the proviso that polymorphic sections cannot appear inside a monomorphic one. A custom data can be attached to this section, that will be returned by close_section.

Sourceval close_section : 'a t -> 'a t option * section_entry list * Univ.ContextSet.t * Sorts.QVar.Set.t * 'a

Close the current section and returns the entries defined inside, the set of global monomorphic constraints added in this section, and the custom data provided at the opening of the section.

Extending sections
Sourceval push_local : Constr.named_declaration -> 'a t -> 'a t

Extend the current section with a local definition (cf. push_named).

Sourceval push_local_universe_context : UVars.UContext.t -> 'a t -> 'a t

Extend the current section with a local universe context. Assumes that the last opened section is polymorphic.

Sourceval push_constraints : Univ.ContextSet.t -> 'a t -> 'a t

Extend the current section with a global universe context. Assumes that the last opened section is monomorphic.

Sourceval push_mono_qualities : Sorts.QVar.Set.t -> 'a t -> 'a t

Extend the current section with a global quality context.

Sourceval push_global : Environ.env -> poly:bool -> section_entry -> 'a t -> 'a t

Push a global entry in this section.

Retrieving section data
Sourceval all_poly_univs : 'a t -> UVars.Instance.t

Returns all polymorphic universes, including those from previous sections. Earlier sections are earlier in the array.

NB: even if the array is empty there may be polymorphic constraints about monomorphic universes, which prevent declaring monomorphic globals.

Sourceval segment_of_constant : Names.Constant.t -> 'a t -> Cooking.cooking_info

Section segment at the time of the constant declaration

Sourceval segment_of_inductive : Names.MutInd.t -> 'a t -> Cooking.cooking_info

Section segment at the time of the inductive declaration

Sourceval is_in_section : Environ.env -> Names.GlobRef.t -> 'a t -> bool