package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.0.tar.gz

sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/coq-core.kernel/IndTyping/index.html

Module `IndTyping`Source

Source

val typecheck_inductive : 
  Environ.env ->
  sec_univs:Univ.Level.t array option ->
  Entries.mutual_inductive_entry ->
  Environ.env
  * Declarations.universes
  * Declarations.template_universes option
  * Univ.Variance.t array option
  * Names.Id.t array option option
  * Constr.rel_context
  * ((Declarations.inductive_arity * Constr.types array)
     * (Constr.rel_context * (Constr.rel_context * Constr.types) array)
     * Sorts.family)
      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)
parameters
for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) * top allowed elimination