🐆 Tx_rollup_l2_qty.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.Int64]
Definition t := Compare.Int64.(Compare.S.t).
Definition op_eq := Compare.Int64.(Compare.S.op_eq).
Definition op_ltgt := Compare.Int64.(Compare.S.op_ltgt).
Definition op_lt := Compare.Int64.(Compare.S.op_lt).
Definition op_lteq := Compare.Int64.(Compare.S.op_lteq).
Definition op_gteq := Compare.Int64.(Compare.S.op_gteq).
Definition op_gt := Compare.Int64.(Compare.S.op_gt).
Definition compare := Compare.Int64.(Compare.S.compare).
Definition equal := Compare.Int64.(Compare.S.equal).
Definition max := Compare.Int64.(Compare.S.max).
Definition min := Compare.Int64.(Compare.S.min).
Definition zero : int64 := 0.
Definition one : int64 := 1.
Definition of_int64 (q_value : t) : option t :=
if op_lt q_value 0 then
None
else
Some q_value.
Definition of_int64_exn (q_value : t) : t :=
match of_int64 q_value with
| Some q_value ⇒ q_value
| None ⇒ Pervasives.invalid_arg "Tx_rollup_l2_qty.of_int64_exn"
end.
Definition to_int64 {A : Set} (q_value : A) : A := q_value.
Definition to_z : int64 → Z.t := Z.of_int64.
Definition to_string (q_value : int64) : string := Int64.to_string q_value.
Definition of_string (q_value : string) : option t :=
Option.bind (Int64.of_string_opt q_value) of_int64.
Definition pp (fmt : Format.formatter) (q_value : int64) : unit :=
Format.pp_print_string fmt (to_string q_value).
Definition compact_encoding : Data_encoding.Compact.t t :=
Data_encoding.Compact.conv None to_int64 of_int64_exn
Data_encoding.Compact.int64_value.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
compact_encoding.
Definition sub (q1 : t) (q2 : t) : option int64 :=
if op_lteq q2 q1 then
Some (q1 -i64 q2)
else
None.
Definition add (q1 : t) (q2 : int64) : option int64 :=
let q_value := q1 +i64 q2 in
if op_lt q_value q1 then
None
else
Some q_value.
Definition succ (q_value : t) : option int64 := add q_value one.
Definition op_minus : t → t → option int64 := sub.
Definition op_plus : t → int64 → option int64 := add.
Definition op_eq := Compare.Int64.(Compare.S.op_eq).
Definition op_ltgt := Compare.Int64.(Compare.S.op_ltgt).
Definition op_lt := Compare.Int64.(Compare.S.op_lt).
Definition op_lteq := Compare.Int64.(Compare.S.op_lteq).
Definition op_gteq := Compare.Int64.(Compare.S.op_gteq).
Definition op_gt := Compare.Int64.(Compare.S.op_gt).
Definition compare := Compare.Int64.(Compare.S.compare).
Definition equal := Compare.Int64.(Compare.S.equal).
Definition max := Compare.Int64.(Compare.S.max).
Definition min := Compare.Int64.(Compare.S.min).
Definition zero : int64 := 0.
Definition one : int64 := 1.
Definition of_int64 (q_value : t) : option t :=
if op_lt q_value 0 then
None
else
Some q_value.
Definition of_int64_exn (q_value : t) : t :=
match of_int64 q_value with
| Some q_value ⇒ q_value
| None ⇒ Pervasives.invalid_arg "Tx_rollup_l2_qty.of_int64_exn"
end.
Definition to_int64 {A : Set} (q_value : A) : A := q_value.
Definition to_z : int64 → Z.t := Z.of_int64.
Definition to_string (q_value : int64) : string := Int64.to_string q_value.
Definition of_string (q_value : string) : option t :=
Option.bind (Int64.of_string_opt q_value) of_int64.
Definition pp (fmt : Format.formatter) (q_value : int64) : unit :=
Format.pp_print_string fmt (to_string q_value).
Definition compact_encoding : Data_encoding.Compact.t t :=
Data_encoding.Compact.conv None to_int64 of_int64_exn
Data_encoding.Compact.int64_value.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
compact_encoding.
Definition sub (q1 : t) (q2 : t) : option int64 :=
if op_lteq q2 q1 then
Some (q1 -i64 q2)
else
None.
Definition add (q1 : t) (q2 : int64) : option int64 :=
let q_value := q1 +i64 q2 in
if op_lt q_value q1 then
None
else
Some q_value.
Definition succ (q_value : t) : option int64 := add q_value one.
Definition op_minus : t → t → option int64 := sub.
Definition op_plus : t → int64 → option int64 := add.