🐆 Tx_rollup_parameters.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.

Module deposit_parameters.
  Record record : Set := Build {
    ex_ticket : Ticket_scanner.ex_ticket;
    l2_destination : Script_typed_ir.tx_rollup_l2_address;
  }.
  Definition with_ex_ticket ex_ticket (r : record) :=
    Build ex_ticket r.(l2_destination).
  Definition with_l2_destination l2_destination (r : record) :=
    Build r.(ex_ticket) l2_destination.
End deposit_parameters.
Definition deposit_parameters := deposit_parameters.record.

Definition get_deposit_parameters {a : Set}
  (function_parameter : Script_typed_ir.ty)
  : Script_typed_ir.pair (Script_typed_ir.ticket a)
    Script_typed_ir.tx_rollup_l2_address → deposit_parameters :=
  match function_parameter with
  |
    Script_typed_ir.Pair_t (Script_typed_ir.Ticket_t ty_value _)
      Script_typed_ir.Tx_rollup_l2_address_t _ _ ⇒
    fun (function_parameter :
      Script_typed_ir.ticket a × Script_typed_ir.tx_rollup_l2_address) ⇒
      let '(ticket, l2_destination) := function_parameter in
      {|
        deposit_parameters.ex_ticket :=
          Ticket_scanner.Ex_ticket ty_value ticket;
        deposit_parameters.l2_destination := l2_destination; |}
  | _ ⇒ unreachable_gadt_branch
  end.