🦏 Sc_rollup_tick_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Definition t : Set := Z.t.
Definition initial : Z.t := Z.zero.
Definition next : Z.t → Z.t := Z.succ.
Definition jump (tick : Z.t) (z_value : Z.t) : Z.t :=
Z.max initial (tick +Z z_value).
Definition pp : Format.formatter → Z.t → unit := Z.pp_print.
Definition encoding : Data_encoding.encoding Z.t := Data_encoding.n_value.
Definition distance (tick1 : Z.t) (tick2 : Z.t) : Z.t := Z.abs (tick1 -Z tick2).
Definition of_int (x_value : int) : option Z.t :=
if x_value <i 0 then
None
else
Some (Z.of_int x_value).
Definition to_int (x_value : Z.t) : option int :=
if Z.fits_int x_value then
Some (Z.to_int x_value)
else
None.
Definition of_z {A : Set} (x_value : A) : A := x_value.
Definition of_number_of_ticks (x_value : Sc_rollup_repr.Number_of_ticks.t)
: Z.t := Z.of_int64 (Sc_rollup_repr.Number_of_ticks.to_value x_value).
Definition op_lteq : Z.t → Z.t → bool := Z.leq.
Definition op_lt : Z.t → Z.t → bool := Z.lt.
Definition op_gteq : Z.t → Z.t → bool := Z.geq.
Definition op_gt : Z.t → Z.t → bool := Z.gt.
Definition op_eq : Z.t → Z.t → bool := Z.equal.
Definition op_ltgt (x_value : Z.t) (y_value : Z.t) : bool :=
Pervasives.not (op_eq x_value y_value).
Definition compare : Z.t → Z.t → int := Z.compare.
Definition equal : Z.t → Z.t → bool := Z.equal.
Definition min : Z.t → Z.t → Z.t := Z.min.
Definition max : Z.t → Z.t → Z.t := Z.max.
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Z.compare
|}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Definition t : Set := Z.t.
Definition initial : Z.t := Z.zero.
Definition next : Z.t → Z.t := Z.succ.
Definition jump (tick : Z.t) (z_value : Z.t) : Z.t :=
Z.max initial (tick +Z z_value).
Definition pp : Format.formatter → Z.t → unit := Z.pp_print.
Definition encoding : Data_encoding.encoding Z.t := Data_encoding.n_value.
Definition distance (tick1 : Z.t) (tick2 : Z.t) : Z.t := Z.abs (tick1 -Z tick2).
Definition of_int (x_value : int) : option Z.t :=
if x_value <i 0 then
None
else
Some (Z.of_int x_value).
Definition to_int (x_value : Z.t) : option int :=
if Z.fits_int x_value then
Some (Z.to_int x_value)
else
None.
Definition of_z {A : Set} (x_value : A) : A := x_value.
Definition of_number_of_ticks (x_value : Sc_rollup_repr.Number_of_ticks.t)
: Z.t := Z.of_int64 (Sc_rollup_repr.Number_of_ticks.to_value x_value).
Definition op_lteq : Z.t → Z.t → bool := Z.leq.
Definition op_lt : Z.t → Z.t → bool := Z.lt.
Definition op_gteq : Z.t → Z.t → bool := Z.geq.
Definition op_gt : Z.t → Z.t → bool := Z.gt.
Definition op_eq : Z.t → Z.t → bool := Z.equal.
Definition op_ltgt (x_value : Z.t) (y_value : Z.t) : bool :=
Pervasives.not (op_eq x_value y_value).
Definition compare : Z.t → Z.t → int := Z.compare.
Definition equal : Z.t → Z.t → bool := Z.equal.
Definition min : Z.t → Z.t → Z.t := Z.min.
Definition max : Z.t → Z.t → Z.t := Z.max.
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Z.compare
|}.