package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type structured_fixpoint_expr = {
  1. fix_name : Names.Id.t;
  2. fix_univs : Constrexpr.universe_decl_expr option;
  3. fix_annot : Names.lident option;
  4. fix_binders : Constrexpr.local_binder_expr list;
  5. fix_body : Constrexpr.constr_expr option;
  6. fix_type : Constrexpr.constr_expr;
}
val interp_recursive : program_mode:bool -> cofix:bool -> structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (Names.Id.t list * EConstr.constr option list * EConstr.types list) * (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
val extract_fixpoint_components : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> structured_fixpoint_expr list * Vernacexpr.decl_notation list
val extract_cofixpoint_components : (Vernacexpr.cofixpoint_expr * Vernacexpr.decl_notation list) list -> structured_fixpoint_expr list * Vernacexpr.decl_notation list
type recursive_preentry = Names.Id.t list * Constr.constr option list * Constr.types list
val compute_possible_guardness_evidences : (('a, 'b) Context.Rel.pt * 'c * int option) -> int list