🎫 Ticket_amount.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.
Require TezosOfOCaml.Proto_alpha.Script_int.

Definition t : Set := Script_int.num.

Definition of_n (n_value : Script_int.num) : option t :=
  if (Script_int.compare n_value Script_int.zero_n) >i 0 then
    Some n_value
  else
    None.

Definition of_z (z_value : Script_int.num) : option t :=
  Option.bind (Script_int.is_nat z_value) of_n.

Definition of_zint (z_value : Z.t) : option t :=
  of_z (Script_int.of_zint z_value).

Definition add : Script_int.num → Script_int.num → Script_int.num :=
  Script_int.add_n.

Definition sub (a_value : Script_int.num) (b_value : Script_int.num)
  : option t := of_z (Script_int.sub a_value b_value).

Definition one : Script_int.num := Script_int.one_n.

Definition encoding : Data_encoding.encoding Script_int.num :=
  Data_encoding.conv_with_guard Script_int.to_zint
    (fun (n_value : Z.t) ⇒
      (fun x_1 ⇒ Option.value_e x_1 "expecting positive number")
        (of_zint n_value)) None Data_encoding.n_value.