🦏 Sc_rollup_metadata_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.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Module t.
Record record : Set := Build {
address : Sc_rollup_repr.Address.t;
origination_level : Raw_level_repr.t;
}.
Definition with_address address (r : record) :=
Build address r.(origination_level).
Definition with_origination_level origination_level (r : record) :=
Build r.(address) origination_level.
End t.
Definition t := t.record.
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
let '{| t.address := address; t.origination_level := origination_level |} :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "address: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " ; origination_level: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"address: %a ; origination_level: %a") Sc_rollup_repr.Address.pp address
Raw_level_repr.pp origination_level.
Definition equal (function_parameter : t) : t → bool :=
let '{| t.address := address; t.origination_level := origination_level |} :=
function_parameter in
fun (metadata2 : t) ⇒
(Sc_rollup_repr.Address.equal address metadata2.(t.address)) &&
(Raw_level_repr.equal origination_level metadata2.(t.origination_level)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.address := address; t.origination_level := origination_level |} :=
function_parameter in
(address, origination_level))
(fun (function_parameter : Sc_rollup_repr.Address.t × Raw_level_repr.t) ⇒
let '(address, origination_level) := function_parameter in
{| t.address := address; t.origination_level := origination_level; |})
None
(Data_encoding.obj2
(Data_encoding.req None None "address" Sc_rollup_repr.Address.encoding)
(Data_encoding.req None None "origination_level" Raw_level_repr.encoding)).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Module t.
Record record : Set := Build {
address : Sc_rollup_repr.Address.t;
origination_level : Raw_level_repr.t;
}.
Definition with_address address (r : record) :=
Build address r.(origination_level).
Definition with_origination_level origination_level (r : record) :=
Build r.(address) origination_level.
End t.
Definition t := t.record.
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
let '{| t.address := address; t.origination_level := origination_level |} :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "address: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " ; origination_level: "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"address: %a ; origination_level: %a") Sc_rollup_repr.Address.pp address
Raw_level_repr.pp origination_level.
Definition equal (function_parameter : t) : t → bool :=
let '{| t.address := address; t.origination_level := origination_level |} :=
function_parameter in
fun (metadata2 : t) ⇒
(Sc_rollup_repr.Address.equal address metadata2.(t.address)) &&
(Raw_level_repr.equal origination_level metadata2.(t.origination_level)).
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let '{|
t.address := address; t.origination_level := origination_level |} :=
function_parameter in
(address, origination_level))
(fun (function_parameter : Sc_rollup_repr.Address.t × Raw_level_repr.t) ⇒
let '(address, origination_level) := function_parameter in
{| t.address := address; t.origination_level := origination_level; |})
None
(Data_encoding.obj2
(Data_encoding.req None None "address" Sc_rollup_repr.Address.encoding)
(Data_encoding.req None None "origination_level" Raw_level_repr.encoding)).