package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

Sourceval declare_prop_but_default_dependent_elim : Names.inductive -> unit

Declare an inductive should be eliminated dependently even though it's in Prop

Sourceval is_prop_but_default_dependent_elim : Names.inductive -> bool

Check if an inductive should be eliminated dependently even though it's in Prop

val pseudo_sort_quality_for_elim : 
  Names.inductive ->
  Declarations.one_inductive_body ->
  Sorts.Quality.t

Legacy API, returns the quality of the inductive except if it's prop_but_default_dependent_elim in which case we return Type instead.

Sourceval default_case_analysis_dependence : Environ.env -> Names.inductive -> bool

Returns false on inductives which cannot be eliminated dependently or are in Prop without being declared prop_but_default_dependent_elim.

val elim_scheme : 
  dep:bool ->
  to_kind:UnivGen.QualityOrSet.t ->
  Ind_tables.individual Ind_tables.scheme_kind

Induction/recursion schemes

Case analysis schemes

Sourceval case_dep : Ind_tables.individual Ind_tables.scheme_kind

Sourceval case_nodep : Ind_tables.individual Ind_tables.scheme_kind

Sourceval casep_dep : Ind_tables.individual Ind_tables.scheme_kind

Sourceval casep_nodep : Ind_tables.individual Ind_tables.scheme_kind

Recursor names utilities

val lookup_eliminator : 
  Environ.env ->
  Names.inductive ->
  UnivGen.QualityOrSet.t ->
  Names.GlobRef.t

Sourceval elimination_suffix : UnivGen.QualityOrSet.t -> string

Sourceval make_elimination_ident : Names.Id.t -> UnivGen.QualityOrSet.t -> Names.Id.t