🐆 Tx_rollup_message_result_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.V7.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_list_hash_repr.

Module t.
  Record record : Set := Build {
    context_hash : Context_hash.t;
    withdraw_list_hash : Tx_rollup_withdraw_list_hash_repr.t;
  }.
  Definition with_context_hash context_hash (r : record) :=
    Build context_hash r.(withdraw_list_hash).
  Definition with_withdraw_list_hash withdraw_list_hash (r : record) :=
    Build r.(context_hash) withdraw_list_hash.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        t.context_hash := context_hash;
          t.withdraw_list_hash := withdraw_list_hash
          |} := function_parameter in
      (context_hash, withdraw_list_hash))
    (fun (function_parameter :
      Context_hash.t × Tx_rollup_withdraw_list_hash_repr.t) ⇒
      let '(context_hash, withdraw_list_hash) := function_parameter in
      {| t.context_hash := context_hash;
        t.withdraw_list_hash := withdraw_list_hash; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "context_hash" Context_hash.encoding)
      (Data_encoding.req None None "withdraw_list_hash"
        Tx_rollup_withdraw_list_hash_repr.encoding)).

Definition empty_l2_context_hash : Context_hash.t :=
  Context_hash.of_b58check_exn
    "CoVu7Pqp1Gh3z33mink5T5Q2kAQKtnn3GHxVhyehdKZpQMBxFBGF".

Definition init_value : t :=
  {| t.context_hash := empty_l2_context_hash;
    t.withdraw_list_hash := Tx_rollup_withdraw_list_hash_repr.empty; |}.