package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Fixpoints and cofixpoints

Entry points for the vernacular commands Fixpoint and CoFixpoint

val do_fixpoint_interactive : scope:Locality.locality -> poly:bool -> ?typing_flags:Declarations.typing_flags -> Vernacexpr.fixpoint_expr list -> Declare.Proof.t
val do_fixpoint : scope:Locality.locality -> poly:bool -> ?typing_flags:Declarations.typing_flags -> ?using:Vernacexpr.section_subset_expr -> Vernacexpr.fixpoint_expr list -> unit
val do_cofixpoint_interactive : scope:Locality.locality -> poly:bool -> Vernacexpr.cofixpoint_expr list -> Declare.Proof.t
val do_cofixpoint : scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> Vernacexpr.cofixpoint_expr list -> unit

Internal API

Typing global fixpoints and cofixpoint_expr

val adjust_rec_order : structonly:bool -> Constrexpr.local_binder_expr list -> Constrexpr.recursion_order_expr option -> Names.lident option
type ('constr, 'types) recursive_preentry = Names.Id.t list * Sorts.relevance list * 'constr option list * 'types list

names / relevance / defs / types

Exported for Program

Exported for Funind

val interp_fixpoint : ?check_recursivity:bool -> ?typing_flags:Declarations.typing_flags -> cofix:bool -> Names.lident option Vernacexpr.fix_expr_gen list -> (Constr.t, Constr.types) 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

Very private function, do not use

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