🦏 Sc_rollup_operations.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.

Module origination_result.
  Record record : Set := Build {
    address : Alpha_context.Sc_rollup.Address.t;
    size : Z.t;
  }.
  Definition with_address address (r : record) :=
    Build address r.(size).
  Definition with_size size (r : record) :=
    Build r.(address) size.
End origination_result.
Definition origination_result := origination_result.record.

Definition originate
  (ctxt : Alpha_context.context) (kind_value : Alpha_context.Sc_rollup.Kind.t)
  (boot_sector : string) : M? (origination_result × Alpha_context.context) :=
  let? '(address, size_value, ctxt) :=
    Alpha_context.Sc_rollup.originate ctxt kind_value boot_sector in
  return?
    ({| origination_result.address := address;
      origination_result.size := size_value; |}, ctxt).