package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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