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

Definition t : Set := Z.t.

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

Definition : Z.t Z.t := Z.succ.

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