🧮 Fixed_point_repr.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Parameter fp_tag : Set.

Parameter integral_tag : Set.

Module Safe.
  Record signature {t : Set} : Set := {
    t := t;
    fp := t;
    integral := t;
    integral_exn : Z.t → integral;
    integral_of_int_exn : int → integral;
    integral_to_z : integral → Z.t;
    zero : t;
    add : t → t → t;
    sub : t → t → t;
    ceil : fp → integral;
    floor : fp → integral;
    fp_value : t → fp;
    op_eq : t → t → bool;
    op_ltgt : t → t → bool;
    op_lt : t → t → bool;
    op_lteq : t → t → bool;
    op_gteq : t → t → bool;
    op_gt : t → t → bool;
    compare : t → t → int;
    equal : t → t → bool;
    max : t → t → t;
    min : t → t → t;
    pp : Format.formatter → t → unit;
    pp_integral : Format.formatter → integral → unit;
    n_fp_encoding : Data_encoding.t fp;
    n_integral_encoding : Data_encoding.t integral;
    z_fp_encoding : Data_encoding.t fp;
    z_integral_encoding : Data_encoding.t integral;
  }.
End Safe.
Definition Safe := @Safe.signature.
Arguments Safe {_}.

Module Full.
  Record signature {t : Set} : Set := {
    t := t;
    fp := t;
    integral := t;
    integral_exn : Z.t → integral;
    integral_of_int_exn : int → integral;
    integral_to_z : integral → Z.t;
    zero : t;
    add : t → t → t;
    sub : t → t → t;
    ceil : fp → integral;
    floor : fp → integral;
    fp_value : t → fp;
    op_eq : t → t → bool;
    op_ltgt : t → t → bool;
    op_lt : t → t → bool;
    op_lteq : t → t → bool;
    op_gteq : t → t → bool;
    op_gt : t → t → bool;
    compare : t → t → int;
    equal : t → t → bool;
    max : t → t → t;
    min : t → t → t;
    pp : Format.formatter → t → unit;
    pp_integral : Format.formatter → integral → unit;
    n_fp_encoding : Data_encoding.t fp;
    n_integral_encoding : Data_encoding.t integral;
    z_fp_encoding : Data_encoding.t fp;
    z_integral_encoding : Data_encoding.t integral;
    unsafe_fp : Z.t → fp;
  }.
End Full.
Definition Full := @Full.signature.
Arguments Full {_}.