🐆 Tx_rollup_parameters.v
Translated 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.
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.