package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz

sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

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

Module `IndTyping`Source

Sourcemodule NotPrimRecordReason : sig ... end

Source

val typecheck_inductive : 
  Environ.env ->
  sec_univs:UVars.Instance.t option ->
  Entries.mutual_inductive_entry ->
  Environ.env
  * Declarations.universes
  * Declarations.template_universes option
  * UVars.Variance.t array option
  * Names.Id.t array option option
  * NotPrimRecordReason.t option
  * Constr.rel_context
  * ((Declarations.inductive_arity * Constr.types array)
     * (Constr.rel_context * (Constr.rel_context * Constr.types) array)
     * Declarations.squash_info option)
      array

Type checking for some inductive entry. Returns:

environment with inductives + parameters in rel context
abstracted universes
checked variance info (variance for section universes is at the beginning of the array)
record entry (checked to be OK)
if primitive record was requested and not ok, the reason why it's not ok
parameters
for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) * top allowed elimination