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

Module `InferCumulativity`Source

val infer_inductive : 
  env_params:Environ.env ->
  env_ar_par:Environ.env ->
  arities:Constr.t list ->
  ctors:Constr.t list list ->
  (Univ.Level.t * Univ.Variance.t option) array ->
  Univ.Variance.t array