package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

Maintainers

E

e@x80.org

Sources

coq-serapi-8.17.0.0.17.3.tbz

sha256=bab246d97c66e06f7a65808a24a295bf288a2b7e07cc45ab4a1e8fc24a1ea3f6

sha512=33dfa7cb9857e30861ef4dc6bd1654799e6fd45d53d7ad9f79755920c1961e67f98f650db1e6dc288f0f1fe744fac28878ec03cce062cae78ae64bdd98614991

doc/src/coq-serapi.serlib/ser_uint63.ml.html

Source file `ser_uint63.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin                                         *)
(* Copyright 2016-2019 MINES ParisTech                                  *)
(* Written by: Emilio J. Gallego Arias                                  *)
(************************************************************************)
(* Status: Very Experimental                                            *)
(************************************************************************)

open Sexplib

type _t = string [@@deriving yojson]
let _t_put = Uint63.to_string
let _t_get x = Uint63.of_int64 (Int64.of_string x)

type t = Uint63.t

let t_of_sexp (x : Sexp.t) : Uint63.t = _t_get (Conv.string_of_sexp x)
let sexp_of_t (x : Uint63.t) : Sexp.t = Conv.sexp_of_string (_t_put x)

let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get)
let to_yojson level = _t_to_yojson (_t_put level)

let hash_fold_t st i =
  Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int64 st (Uint63.to_int64 i)

let compare i1 i2 =
  Ppx_compare_lib.Builtin.compare_int64 (Uint63.to_int64 i1) (Uint63.to_int64 i2)