package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t =
  1. | Int63head0
  2. | Int63tail0
  3. | Int63add
  4. | Int63sub
  5. | Int63mul
  6. | Int63div
  7. | Int63mod
  8. | Int63divs
  9. | Int63mods
  10. | Int63lsr
  11. | Int63lsl
  12. | Int63asr
  13. | Int63land
  14. | Int63lor
  15. | Int63lxor
  16. | Int63addc
  17. | Int63subc
  18. | Int63addCarryC
  19. | Int63subCarryC
  20. | Int63mulc
  21. | Int63diveucl
  22. | Int63div21
  23. | Int63addMulDiv
  24. | Int63eq
  25. | Int63lt
  26. | Int63le
  27. | Int63lts
  28. | Int63les
  29. | Int63compare
  30. | Int63compares
  31. | Float64opp
  32. | Float64abs
  33. | Float64eq
  34. | Float64lt
  35. | Float64le
  36. | Float64compare
  37. | Float64classify
  38. | Float64add
  39. | Float64sub
  40. | Float64mul
  41. | Float64div
  42. | Float64sqrt
  43. | Float64ofUint63
  44. | Float64normfr_mantissa
  45. | Float64frshiftexp
  46. | Float64ldshiftexp
  47. | Float64next_up
  48. | Float64next_down
  49. | Arraymake
  50. | Arrayget
  51. | Arraydefault
  52. | Arrayset
  53. | Arraycopy
  54. | Arraylength
val parse : string -> t

Can raise Not_found. Beware that this is not exactly the reverse of to_string below.

val equal : t -> t -> bool
type const =
  1. | Arraymaxlength
type arg_kind =
  1. | Kparam
  2. | Kwhnf
  3. | Karg
type args_red = arg_kind list
val hash : t -> int
val to_string : t -> string
val arity : t -> int

Including parameters

val nparams : t -> int
val kind : t -> args_red

Includes parameters

Special Entries for Register *

type 'a prim_type =
  1. | PT_int63 : unit prim_type
  2. | PT_float64 : unit prim_type
  3. | PT_array : (Univ.Instance.t * ind_or_type) prim_type
and 'a prim_ind =
  1. | PIT_bool : unit prim_ind
  2. | PIT_carry : ind_or_type prim_ind
  3. | PIT_pair : (ind_or_type * ind_or_type) prim_ind
  4. | PIT_cmp : unit prim_ind
  5. | PIT_f_cmp : unit prim_ind
  6. | PIT_f_class : unit prim_ind
and ind_or_type =
  1. | PITT_ind : 'a prim_ind * 'a -> ind_or_type
  2. | PITT_type : 'a prim_type * 'a -> ind_or_type
  3. | PITT_param : int -> ind_or_type
val typ_univs : 'a prim_type -> Univ.AUContext.t
type prim_type_ex =
  1. | PTE : 'a prim_type -> prim_type_ex
type prim_ind_ex =
  1. | PIE : 'a prim_ind -> prim_ind_ex
val prim_type_of_string : string -> prim_type_ex

Can raise Not_found

val prim_type_to_string : 'a prim_type -> string
type op_or_type =
  1. | OT_op of t
  2. | OT_type : 'a prim_type -> op_or_type
  3. | OT_const of const
val op_or_type_univs : op_or_type -> Univ.AUContext.t
val prim_ind_to_string : 'a prim_ind -> string
val op_or_type_of_string : string -> op_or_type

Can raise Not_found

val op_or_type_to_string : op_or_type -> string
val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
val univs : t -> Univ.AUContext.t

Parameters * Reduction relevant arguments * output type

XXX we could reify universes in ind_or_type (currently polymorphic types like array are assumed to use universe 0).

val body_of_prim_const : const -> Constr.t
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