🐆 Tx_rollup_withdraw_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.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.

Module order.
  Record record : Set := Build {
    claimer : Signature.public_key_hash;
    ticket_hash : Ticket_hash_repr.t;
    amount : Tx_rollup_l2_qty.t;
  }.
  Definition with_claimer claimer (r : record) :=
    Build claimer r.(ticket_hash) r.(amount).
  Definition with_ticket_hash ticket_hash (r : record) :=
    Build r.(claimer) ticket_hash r.(amount).
  Definition with_amount amount (r : record) :=
    Build r.(claimer) r.(ticket_hash) amount.
End order.
Definition order := order.record.

Definition t : Set := order.

Definition encoding : Data_encoding.t t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        order.claimer := claimer;
          order.ticket_hash := ticket_hash;
          order.amount := amount
          |} := function_parameter in
      (claimer, ticket_hash, amount))
    (fun (function_parameter :
      Signature.public_key_hash × Ticket_hash_repr.t × Tx_rollup_l2_qty.t) ⇒
      let '(claimer, ticket_hash, amount) := function_parameter in
      {| order.claimer := claimer; order.ticket_hash := ticket_hash;
        order.amount := amount; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None None "claimer"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "ticket_hash" Ticket_hash_repr.encoding)
      (Data_encoding.req None None "amount" Tx_rollup_l2_qty.encoding)).