👔 Manager_counter_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.V8.

Inclusion of the module [Compare.Z]

Definition t := Compare.Z.(Compare.S.t).

Definition op_eq := Compare.Z.(Compare.S.op_eq).

Definition op_ltgt := Compare.Z.(Compare.S.op_ltgt).

Definition op_lt := Compare.Z.(Compare.S.op_lt).

Definition op_lteq := Compare.Z.(Compare.S.op_lteq).

Definition op_gteq := Compare.Z.(Compare.S.op_gteq).

Definition op_gt := Compare.Z.(Compare.S.op_gt).

Definition compare := Compare.Z.(Compare.S.compare).

Definition equal := Compare.Z.(Compare.S.equal).

Definition max := Compare.Z.(Compare.S.max).

Definition min := Compare.Z.(Compare.S.min).

Definition init_value : Z.t := Z.zero.

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

Definition pp : Format.formatter → Z.t → unit := Z.pp_print.

Definition encoding_for_storage : Data_encoding.encoding Z.t :=
  Data_encoding.z_value.

Definition encoding_for_operation : Data_encoding.encoding Z.t :=
  Data_encoding.check_size 10 Data_encoding.n_value.

Definition encoding_for_RPCs : Data_encoding.encoding Z.t :=
  Data_encoding.n_value.

Definition encoding_for_errors : Data_encoding.encoding Z.t :=
  Data_encoding.z_value.

Module Internal_for_injection.
  Definition of_string (s_value : string) : option Z.t :=
    let 'z_value := Z.of_string s_value in
    if op_lt z_value Z.zero then
      None
    else
      Some z_value.
End Internal_for_injection.