👔 Manager_counter_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
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.