package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ElimschemesSource

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

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.

Induction/recursion schemes

Case analysis schemes

Recursor names utilities

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