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.16.1.tar.gz

sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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