package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Errors related to recursors building

type recursion_scheme_error =
  1. | NotAllowedCaseAnalysis of bool * Sorts.t * Constr.pinductive
  2. | NotMutualInScheme of Names.inductive * Names.inductive
  3. | NotAllowedDependentAnalysis of bool * Names.inductive
exception RecursionSchemeError of Environ.env * recursion_scheme_error

Eliminations

type dep_flag = bool

Build a case analysis elimination scheme in some sort

type case_analysis = private {
  1. case_params : EConstr.rel_context;
  2. case_pred : Names.Name.t EConstr.binder_annot * EConstr.types;
  3. case_branches : EConstr.rel_context;
  4. case_arity : EConstr.rel_context;
  5. case_body : EConstr.t;
  6. case_type : EConstr.t;
}
val check_valid_elimination : Environ.env -> Evd.evar_map -> Names.inductive EConstr.puniverses -> dep:bool -> EConstr.ESorts.t -> unit
val eval_case_analysis : case_analysis -> EConstr.t * EConstr.types
val default_case_analysis_dependence : Environ.env -> Names.inductive -> bool

Build a dependent case elimination predicate unless type is in Prop or is a recursive record with primitive projections.

Builds a recursive induction scheme (Peano-induction style) in the given sort.

Builds mutual (recursive) induction schemes

val build_mutual_induction_scheme : Environ.env -> Evd.evar_map -> ?force_mutual:bool -> (Names.inductive EConstr.puniverses * dep_flag * EConstr.ESorts.t) list -> Evd.evar_map * EConstr.constr list

Recursor names utilities

val lookup_eliminator : Environ.env -> Names.inductive -> Sorts.family -> Names.GlobRef.t
val elimination_suffix : Sorts.family -> string
val make_elimination_ident : Names.Id.t -> Sorts.family -> Names.Id.t
val case_suffix : string

Default dependence of eliminations for Prop inductives

val declare_prop_but_default_dependent_elim : Names.inductive -> unit
val is_prop_but_default_dependent_elim : Names.inductive -> bool
val pseudo_sort_family_for_elim : Names.inductive -> Declarations.one_inductive_body -> Sorts.family
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct