Module IndTyping

val typecheck_inductive : Environ.env -> Entries.mutual_inductive_entry -> Environ.env * Declarations.universes * 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 list) array

Type checking for some inductive entry. Returns:

  • environment with inductives + parameters in rel context
  • abstracted universes
  • checked variance info
  • record entry (checked to be OK)
  • parameters
  • for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) * allowed eliminations
val template_polymorphic_univs : template_check:bool -> ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> Univ.Level.t option list * Univ.LSet.t