coq-serapi 8.20.0+0.20.0 (latest)

coq-serapi

module UVars = Ser_uvars

type 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
| Float64equal
| Float64classify
| Float64add
| Float64sub
| Float64mul
| Float64div
| Float64sqrt
| Float64ofUint63
| Float64normfr_mantissa
| Float64frshiftexp
| Float64ldshiftexp
| Float64next_up
| Float64next_down
| Arraymake
| Arrayget
| Arraydefault
| Arrayset
| Arraycopy
| Arraylength
| Stringmake
| Stringlength
| Stringget
| Stringsub
| Stringcat
| Stringcompare

val t_of_sexp : Sexplib0.Sexp.t -> t

val sexp_of_t : t -> Sexplib0.Sexp.t

val to_yojson : t -> Yojson.Safe.t

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

val hash_fold_t : Base.Hash.state -> t -> Base.Hash.state

val hash : t -> Base.Hash.hash_value

val compare : t -> t -> int

type const = CPrimitives.const =

| Arraymaxlength
| Stringmaxlength

val const_of_sexp : Sexplib0.Sexp.t -> const

val sexp_of_const : const -> Sexplib0.Sexp.t

val const_to_yojson : const -> Yojson.Safe.t

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

val hash_fold_const : Base.Hash.state -> const -> Base.Hash.state

val hash_const : const -> Base.Hash.hash_value

val compare_const : const -> const -> int

module PTP : sig ... end

module Prim_type_ : sig ... end

type 'a prim_type = 'a Prim_type_.t

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

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

val prim_type_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a prim_type ->
  Yojson.Safe.t

val prim_type_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a prim_type Ppx_deriving_yojson_runtime.error_or

val hash_fold_prim_type : 
  'a. (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a prim_type ->
  Base.Hash.state

val compare_prim_type : 
  'a. ('a -> 'a -> int) ->
  'a prim_type ->
  'a prim_type ->
  int

module OOTP : sig ... end

module Op_or_type_ : sig ... end

type op_or_type = Op_or_type_.t

val op_or_type_of_sexp : Sexplib0.Sexp.t -> op_or_type

val sexp_of_op_or_type : op_or_type -> Sexplib0.Sexp.t

val op_or_type_to_yojson : op_or_type -> Yojson.Safe.t

val op_or_type_of_yojson : 
  Yojson.Safe.t ->
  op_or_type Ppx_deriving_yojson_runtime.error_or

val _ : Yojson.Safe.t -> op_or_type Ppx_deriving_yojson_runtime.error_or

val hash_fold_op_or_type : Base.Hash.state -> op_or_type -> Base.Hash.state

val hash_op_or_type : op_or_type -> Base.Hash.hash_value

val compare_op_or_type : op_or_type -> op_or_type -> int

package coq-serapi