package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

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 * UVars.Variance.t option) array ->
  UVars.Variance.t array