package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val do_fixpoint_interactive : scope:DeclareDef.locality -> poly:bool -> Vernacexpr.fixpoint_expr list -> Lemmas.t
val do_fixpoint : scope:DeclareDef.locality -> poly:bool -> Vernacexpr.fixpoint_expr list -> unit
val do_cofixpoint_interactive : scope:DeclareDef.locality -> poly:bool -> Vernacexpr.cofixpoint_expr list -> Lemmas.t
val do_cofixpoint : scope:DeclareDef.locality -> poly:bool -> Vernacexpr.cofixpoint_expr list -> unit
val adjust_rec_order : structonly:bool -> Constrexpr.local_binder_expr list -> Constrexpr.recursion_order_expr option -> Names.lident option
val interp_recursive : program_mode:bool -> cofix:bool -> Names.lident option Vernacexpr.fix_expr_gen list -> (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (Names.Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) * (EConstr.rel_context * Impargs.manual_implicits * int option) list
type recursive_preentry = Names.Id.t list * Sorts.relevance list * Constr.constr option list * Constr.types list
val interp_fixpoint : cofix:bool -> Names.lident option Vernacexpr.fix_expr_gen list -> recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list
val compute_possible_guardness_evidences : (('a, 'b) Context.Rel.pt * 'c * int option) -> int list
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