🦏 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)).