Module `Serlib.Ser_cPrimitives`Source

Sourcetype t = CPrimitives.t =

| Int63head0
| Int63tail0
| Int63add
| Int63sub
| Int63mul
| Int63div
| Int63mod
| Int63divs
| Int63mods
| Int63lsr
| Int63lsl
| Int63asr
| Int63land
| Int63lor
| Int63lxor
| Int63addc
| Int63subc
| Int63addCarryC
| Int63subCarryC
| Int63mulc
| Int63diveucl
| Int63div21
| Int63addMulDiv
| Int63eq
| Int63lt
| Int63le
| Int63lts
| Int63les
| Int63compare
| Int63compares
| Float64opp
| Float64abs
| Float64eq
| Float64lt
| Float64le
| Float64compare
| Float64classify
| Float64add
| Float64sub
| Float64mul
| Float64div
| Float64sqrt
| Float64ofUint63
| Float64normfr_mantissa
| Float64frshiftexp
| Float64ldshiftexp
| Float64next_up
| Float64next_down
| Arraymake
| Arrayget
| Arraydefault
| Arrayset
| Arraycopy
| Arraylength

Sourceval t_of_sexp : Sexplib0.Sexp.t -> t

Sourceval sexp_of_t : t -> Sexplib0.Sexp.t

Sourceval to_yojson : t -> Yojson.Safe.t

Sourceval of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val hash_fold_t : 
  Ppx_hash_lib.Std.Hash.state ->
  t ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash : t -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare : t -> t -> int

Sourcetype const = CPrimitives.const =

| Arraymaxlength

Sourceval const_of_sexp : Sexplib0.Sexp.t -> const

Sourceval sexp_of_const : const -> Sexplib0.Sexp.t

Sourceval const_to_yojson : const -> Yojson.Safe.t

Source

val const_of_yojson : 
  Yojson.Safe.t ->
  const Ppx_deriving_yojson_runtime.error_or

Sourceval _ : Yojson.Safe.t -> const Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_const : 
  Ppx_hash_lib.Std.Hash.state ->
  const ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_const : const -> Ppx_hash_lib.Std.Hash.hash_value

Sourcetype 'a prim_type = 'a CPrimitives.prim_type =

| PT_int63 : unit prim_type
| PT_float64 : unit prim_type
| PT_array : (Univ.Instance.t * ind_or_type) prim_type

Sourceand 'a prim_ind = 'a CPrimitives.prim_ind =

| PIT_bool : unit prim_ind
| PIT_carry : ind_or_type prim_ind
| PIT_pair : (ind_or_type * ind_or_type) prim_ind
| PIT_cmp : unit prim_ind
| PIT_f_cmp : unit prim_ind
| PIT_f_class : unit prim_ind

Sourceand ind_or_type = CPrimitives.ind_or_type =

| PITT_ind : 'a prim_ind * 'a -> ind_or_type
| PITT_type : 'a prim_type * 'a -> ind_or_type
| PITT_param : int -> ind_or_type

Source

val sexp_of_prim_type : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a prim_type ->
  Sexplib0.Sexp.t

Source

val sexp_of_prim_ind : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a prim_ind ->
  Sexplib0.Sexp.t

Sourceval sexp_of_ind_or_type : ind_or_type -> Sexplib0.Sexp.t

Sourceval prim_type_of_sexp : Sexplib.Sexp.t -> unit prim_type

Sourcetype op_or_type = CPrimitives.op_or_type =

| OT_op of t
| OT_type : 'a prim_type -> op_or_type
| OT_const of const

Sourceval sexp_of_op_or_type : op_or_type -> Sexplib0.Sexp.t

Sourceval hash_fold_op_or_type : Base__Hash.state -> op_or_type -> Base__Hash.state

Sourceval compare_op_or_type : op_or_type -> op_or_type -> int

Sourceval op_or_type_of_sexp : Sexplib.Sexp.t -> op_or_type

Sourceval op_or_type_to_yojson : 'a -> 'b

Sourceval op_or_type_of_yojson : 'a -> 'b

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-serapi.serlib/Serlib/Ser_cPrimitives/index.html

Module `Serlib.Ser_cPrimitives`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-serapi.serlib/Serlib/Ser_cPrimitives/index.html

Module Serlib.Ser_cPrimitivesSource

Module `Serlib.Ser_cPrimitives`Source