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 family

type case_analysis = private {
  1. case_params : EConstr.rel_context;
  2. case_pred : Names.Name.t Context.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 -> Constr.pinductive -> dep:bool -> Sorts.family -> 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.

val build_case_analysis_scheme_default : Environ.env -> Evd.evar_map -> Constr.pinductive -> Sorts.family -> Evd.evar_map * case_analysis

Builds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop or a recursive record with primitive projections.

Builds mutual (recursive) induction schemes

val build_mutual_induction_scheme : Environ.env -> Evd.evar_map -> ?force_mutual:bool -> (Constr.pinductive * dep_flag * Sorts.family) list -> Evd.evar_map * Constr.constr list

Scheme combinators

weaken_sort_scheme env sigma eq s n c t derives by subtyping from c:t whose conclusion is quantified on Type i at position n of t a scheme quantified on sort s. set asks for s be declared equal to i, otherwise just less or equal to i.

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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