package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587

doc/coq-core.kernel/CPrimitives/index.html

Module CPrimitivesSource

Sourcetype 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. | Float64equal
  38. | Float64classify
  39. | Float64add
  40. | Float64sub
  41. | Float64mul
  42. | Float64div
  43. | Float64sqrt
  44. | Float64ofUint63
  45. | Float64normfr_mantissa
  46. | Float64frshiftexp
  47. | Float64ldshiftexp
  48. | Float64next_up
  49. | Float64next_down
  50. | Arraymake
  51. | Arrayget
  52. | Arraydefault
  53. | Arrayset
  54. | Arraycopy
  55. | Arraylength
Sourceval parse : string -> t

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

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

Including parameters

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

Includes parameters

Special Entries for Register *

Sourcetype '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
Sourceand '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
Sourceand 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
Sourcetype prim_type_ex =
  1. | PTE : 'a prim_type -> prim_type_ex
Sourcetype prim_ind_ex =
  1. | PIE : 'a prim_ind -> prim_ind_ex
Sourceval prim_type_of_string : string -> prim_type_ex

Can raise Not_found

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

Can raise Not_found

Sourceval op_or_type_to_string : op_or_type -> string
Sourceval parse_op_or_type : ?loc:Loc.t -> string -> op_or_type

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).

Sourceval 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