Up – Package index » coq » Library coq-core.kernel » IndTyping

Module `IndTyping`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

Source

val template_polymorphic_univs : 
  ctor_levels:Univ.LSet.t ->
  Univ.ContextSet.t ->
  Constr.rel_context ->
  Univ.Universe.t ->
  (Univ.LSet.t * Univ.Level.t option list) option