🇿 Zk_rollup_ticket_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.

Module t.
  Record record : Set := Build {
    contents : Script_repr.expr;
    ty : Script_repr.expr;
    ticketer : Contract_repr.t;
  }.
  Definition with_contents contents (r : record) :=
    Build contents r.(ty) r.(ticketer).
  Definition with_ty ty (r : record) :=
    Build r.(contents) ty r.(ticketer).
  Definition with_ticketer ticketer (r : record) :=
    Build r.(contents) r.(ty) ticketer.
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 |} :=
        function_parameter in
      (contents, ty_value, ticketer))
    (fun (function_parameter :
      Script_repr.expr × Script_repr.expr × Contract_repr.t) ⇒
      let '(contents, ty_value, ticketer) := function_parameter in
      {| t.contents := contents; t.ty := ty_value; t.ticketer := ticketer; |})
    None
    (Data_encoding.obj3
      (Data_encoding.req None None "contents" Script_repr.expr_encoding)
      (Data_encoding.req None None "ty" Script_repr.expr_encoding)
      (Data_encoding.req None None "ticketer" Contract_repr.encoding)).