package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module ArgT : sig ... end
type (!_, !_, !_) genarg_type =
  1. | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
  2. | ListArg : ('a0, 'b0, 'c0) genarg_type -> ('a0 list, 'b0 list, 'c0 list) genarg_type
  3. | OptArg : ('a1, 'b1, 'c1) genarg_type -> ('a1 option, 'b1 option, 'c1 option) genarg_type
  4. | PairArg : ('a10, 'b10, 'c10) genarg_type * ('a2, 'b2, 'c2) genarg_type -> ('a10 * 'a2, 'b10 * 'b2, 'c10 * 'c2) genarg_type
type !'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
val make0 : string -> ('raw, 'glob, 'top) genarg_type
val create_arg : string -> ('raw, 'glob, 'top) genarg_type
type rlevel = [
  1. | `rlevel
]
type glevel = [
  1. | `glevel
]
type tlevel = [
  1. | `tlevel
]
type (!_, !_) abstract_argument_type =
  1. | Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
  2. | Glbwit : ('a0, 'b0, 'c0) genarg_type -> ('b0, glevel) abstract_argument_type
  3. | Topwit : ('a1, 'b1, 'c1) genarg_type -> ('c1, tlevel) abstract_argument_type
type !'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
type !'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type
type !'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type
val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
type !'l0 generic_argument =
  1. | GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument
val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a
val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
type argument_type =
  1. | ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
val argument_type_eq : argument_type -> argument_type -> bool
val genarg_type_eq : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
val abstract_argument_type_eq : ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> ('a, 'b) CSig.eq option
val pr_argument_type : argument_type -> Pp.t
val genarg_tag : 'a generic_argument -> argument_type
val unquote : ('a, 'co) abstract_argument_type -> argument_type
val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag
module type GenObj = sig ... end
module Register (M : GenObj) : sig ... end
val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
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