package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val set_drawinstr : unit -> unit
type tcode
type vprod
type vfun
type vfix
type vcofix
type vblock
type vswitch
type arguments
type atom =
  1. | Aid of Vars.id_key
  2. | Aind of Names.inductive
  3. | Atype of Univ.universe
type zipper =
  1. | Zapp of arguments
  2. | Zfix of vfix * arguments
  3. | Zswitch of vswitch
  4. | Zproj of Names.Constant.t
type stack = zipper list
type to_up
type whd =
  1. | Vsort of Term.sorts
  2. | Vprod of vprod
  3. | Vfun of vfun
  4. | Vfix of vfix * arguments option
  5. | Vcofix of vcofix * to_up * arguments option
  6. | Vconstr_const of int
  7. | Vconstr_block of vblock
  8. | Vatom_stk of atom * stack
  9. | Vuniv_level of Univ.universe_level
val pr_atom : atom -> Pp.std_ppcmds
val pr_whd : whd -> Pp.std_ppcmds
val pr_stack : stack -> Pp.std_ppcmds
val val_of_rel : int -> Term.values
val val_of_named : Names.Id.t -> Term.values
val val_of_constant : Names.constant -> Term.values
val val_of_annot_switch : Cbytecodes.annot_switch -> Term.values
val whd_val : Term.values -> whd
val uni_lvl_val : Term.values -> Univ.universe_level
val nargs : arguments -> int
val arg : arguments -> int -> Term.values
val dom : vprod -> Term.values
val codom : vprod -> vfun
val body_of_vfun : int -> vfun -> Term.values
val decompose_vfun2 : int -> vfun -> vfun -> int * Term.values * Term.values
val current_fix : vfix -> int
val check_fix : vfix -> vfix -> bool
val rec_args : vfix -> int array
val reduce_fix : int -> vfix -> vfun array * Term.values array
val current_cofix : vcofix -> int
val check_cofix : vcofix -> vcofix -> bool
val reduce_cofix : int -> vcofix -> Term.values array * Term.values array
val btag : vblock -> int
val bsize : vblock -> int
val bfield : vblock -> int -> Term.values
val check_switch : vswitch -> vswitch -> bool
val case_info : vswitch -> Term.case_info
val type_of_switch : vswitch -> Term.values
val branch_of_switch : int -> vswitch -> (int * Term.values) array
val apply_whd : int -> whd -> Term.values
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