Skip to main content

🧮 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.Proto_alpha.Environment.

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 {_}.