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

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.engine/PolyFlags/index.html

Module PolyFlagsSource

Sourcetype t

Set of flags for universe polymorphism, implicit sort polymorphism and cumulativity. Note that implicit sort polymorphism (not collapsing sort variables to Type) and cumulativity only make sense for constructions that are already polymorphic. This invariant is ensured by the smart constructor below.

Sourceval make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> t

Raises a user error if univ_poly = false and either collapse_sort_variables = false or cumulative = true.

Sourceval default : t

The default is monomorphic: univ_poly and cumulative are false, collapse_sort_variables is true

Sourceval of_univ_poly : bool -> t

Only sets the universe univ_poly flag. Use with care, this probably indicates that the code does not handle cumulative constructions when it should. Code relying on elaboration should also support the collapse_sort_variables flag.

Sourceval univ_poly : t -> bool

Accessors

Sourceval collapse_sort_variables : t -> bool
Sourceval cumulative : t -> bool
Sourceval pr : t -> Pp.t

Pretty print

Sourcetype construction_kind =
  1. | Assumption
  2. | Definition
  3. | Inductive

Used to have distinguished default behaviors when treating assumptions/axioms, definitions or inductives