Skip to main content

🦏 Sc_rollup_tick_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.

Definition t : Set := Z.t.

Definition initial : Z.t := Z.zero.

Definition : 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
    |}.