Skip to main content

🐆 Tx_rollup_l2_qty.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.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_valueq_value
  | NonePervasives.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.