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.kernel/Inductive/index.html

Module InductiveSource

Extracting an inductive type from a construction

find_m*type env sigma c coerce c to an recursive type (I args). find_rectype, find_inductive and find_coinductive respectively accepts any recursive type, only an inductive type and only a coinductive type. They raise Not_found if not convertible to a recursive type.

Fetching information in the environment about an inductive type. Raises an anomaly if the inductive type is not found.

Returns the parameters of an inductive type with universes instantiated

Returns the parameters of an inductive type with universes instantiated, splitting it into the contexts of recursively uniform and recursively non-uniform parameters

Sourcetype template_univ =
  1. | TemplateProp
  2. | TemplateUniv of Univ.Universe.t
Sourcetype param_univs = (expected:Univ.Level.t -> template_univ) list
Sourceval relevance_of_ind_body : Declarations.one_inductive_body -> UVars.Instance.t -> Sorts.relevance
Sourceval relevance_of_inductive : Environ.env -> Constr.pinductive -> Sorts.relevance
Sourceval quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool

For squashing.

Sourcetype squash =
  1. | SquashToSet
  2. | SquashToQuality of Sorts.Quality.t
Sourceval is_allowed_elimination : Declarations.mind_specif UVars.puniverses -> Sorts.t -> bool
Sourceval is_private : Declarations.mind_specif -> bool
Sourceval is_primitive_record : Declarations.mind_specif -> bool

Return type as quoted by the user

Sourceval arities_of_constructors : Constr.pinductive -> Declarations.mind_specif -> Constr.types array

Return constructor types in normal form

Sourceval type_of_constructors : Constr.pinductive -> Declarations.mind_specif -> Constr.types array

Return constructor types in user form

Sourceval abstract_constructor_type_relatively_to_inductive_types_context : int -> Names.MutInd.t -> Constr.types -> Constr.types

Turns a constructor type recursively referring to inductive types into the same constructor type referring instead to a context made from the abstract declaration of the inductive types (e.g. turns nat->nat into mkArrowR (Rel 1) (Rel 2)); takes as arguments the number of inductive types in the block and the name of the block

Sourceval inductive_params : Declarations.mind_specif -> int

Given an inductive type and its parameters, builds the context of the return clause, including the inductive being eliminated. The additional binder array is only used to set the names of the context variables, we use the less general type to make it easy to use this function on Case nodes.

Sourceval expand_branch_contexts : Declarations.mind_specif -> UVars.Instance.t -> Constr.constr array -> (Names.Name.t Constr.binder_annot array * 'a) array -> Constr.rel_context array

Given an inductive type and its parameters, builds the context of the return clause, including the inductive being eliminated. The additional binder array is only used to set the names of the context variables, we use the less general type to make it easy to use this function on Case nodes.

Sourcetype ('constr, 'types, 'r) pexpanded_case = Constr.case_info * ('constr * 'r) * 'constr Constr.pcase_invert * 'constr * 'constr array

Given a pattern-matching represented compactly, expands it so as to produce lambda and let abstractions in front of the return clause and the pattern branches.

Sourceval contract_case : Environ.env -> expanded_case -> Constr.case

Dual operation of the above. Fails if the return clause or branch has not the expected form.

instantiate_context u subst nas ctx applies both u and subst to ctx while replacing names using nas (order reversed). In particular, assumes that ctx and nas have the same length.

Sourceval check_case_info : Environ.env -> Constr.pinductive -> Constr.case_info -> unit

Check a case_info actually correspond to a Case expression on the given inductive type.

Guard conditions for fix and cofix-points.
Sourceval is_primitive_positive_container : Environ.env -> Names.Constant.t -> bool

is_primitive_positive_container env c tells if the constant c is registered as a primitive type that can be seen as a container where the occurrences of its parameters are positive, in which case the positivity and guard conditions are extended to allow inductive types to nest their subterms in these containers.

Sourceval check_fix : ?evars:CClosure.evar_handler -> Environ.env -> Constr.fixpoint -> unit

When chk is false, the guard condition is not actually checked.

Sourceval check_cofix : ?evars:CClosure.evar_handler -> Environ.env -> Constr.cofixpoint -> unit
Sourceval abstract_mind_lc : int -> int -> Names.MutInd.t -> (Constr.rel_context * Constr.constr) array -> Constr.constr array