🐆 Tx_rollup_reveal_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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.

Module t.
  Record record : Set := Build {
    contents : Script_repr.lazy_expr;
    ty : Script_repr.lazy_expr;
    ticketer : Contract_repr.t;
    amount : Tx_rollup_l2_qty.t;
    claimer : Signature.public_key_hash;
  }.
  Definition with_contents contents (r : record) :=
    Build contents r.(ty) r.(ticketer) r.(amount) r.(claimer).
  Definition with_ty ty (r : record) :=
    Build r.(contents) ty r.(ticketer) r.(amount) r.(claimer).
  Definition with_ticketer ticketer (r : record) :=
    Build r.(contents) r.(ty) ticketer r.(amount) r.(claimer).
  Definition with_amount amount (r : record) :=
    Build r.(contents) r.(ty) r.(ticketer) amount r.(claimer).
  Definition with_claimer claimer (r : record) :=
    Build r.(contents) r.(ty) r.(ticketer) r.(amount) claimer.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.t t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        t.contents := contents;
          t.ty := ty_value;
          t.ticketer := ticketer;
          t.amount := amount;
          t.claimer := claimer
          |} := function_parameter in
      (contents, ty_value, ticketer, amount, claimer))
    (fun (function_parameter :
      Script_repr.lazy_expr × Script_repr.lazy_expr × Contract_repr.t ×
        Tx_rollup_l2_qty.t × Signature.public_key_hash) ⇒
      let '(contents, ty_value, ticketer, amount, claimer) := function_parameter
        in
      {| t.contents := contents; t.ty := ty_value; t.ticketer := ticketer;
        t.amount := amount; t.claimer := claimer; |}) None
    (Data_encoding.obj5
      (Data_encoding.req None None "contents" Script_repr.lazy_expr_encoding)
      (Data_encoding.req None None "ty" Script_repr.lazy_expr_encoding)
      (Data_encoding.req None None "ticketer" Contract_repr.encoding)
      (Data_encoding.req None None "amount" Tx_rollup_l2_qty.encoding)
      (Data_encoding.req None None "claimer"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))).