🐆 Tx_rollup_message_result_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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; |}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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; |}.