package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
val template_polymorphic_univs : ctor_levels:Univ.Level.Set.t -> Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> (Univ.Level.Set.t * Univ.Level.t option list) option