🐆 Tx_rollup_storage.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.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Definition fresh_tx_rollup_from_current_nonce (ctxt : Raw_context.t)
: M? (Raw_context.t × Tx_rollup_repr.t) :=
let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
return? (ctxt, (Tx_rollup_repr.originated_tx_rollup nonce_value)).
Definition originate (ctxt : Raw_context.t)
: M? (Raw_context.t × Tx_rollup_repr.t) :=
let? '(ctxt, tx_rollup) := fresh_tx_rollup_from_current_nonce ctxt in
let? ctxt := Tx_rollup_state_storage.init_value ctxt tx_rollup in
return? (ctxt, tx_rollup).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Definition fresh_tx_rollup_from_current_nonce (ctxt : Raw_context.t)
: M? (Raw_context.t × Tx_rollup_repr.t) :=
let? '(ctxt, nonce_value) := Raw_context.increment_origination_nonce ctxt in
return? (ctxt, (Tx_rollup_repr.originated_tx_rollup nonce_value)).
Definition originate (ctxt : Raw_context.t)
: M? (Raw_context.t × Tx_rollup_repr.t) :=
let? '(ctxt, tx_rollup) := fresh_tx_rollup_from_current_nonce ctxt in
let? ctxt := Tx_rollup_state_storage.init_value ctxt tx_rollup in
return? (ctxt, tx_rollup).