🏗️ Apply_results.v

Translated OCaml

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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_operation_result.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.

Definition successful_transaction_result : Set :=
  Apply_internal_results.successful_transaction_result.

Definition successful_origination_result : Set :=
  Apply_internal_results.successful_origination_result.

Records for the constructor parameters

Module ConstructorRecords_successful_manager_operation_result.
  Module successful_manager_operation_result.
    Module Reveal_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Reveal_result.
    Definition Reveal_result_skeleton := Reveal_result.record.

    Module Delegation_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Delegation_result.
    Definition Delegation_result_skeleton := Delegation_result.record.

    Module Register_global_constant_result.
      Record record {balance_updates consumed_gas size_of_constant
        global_address : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        size_of_constant : size_of_constant;
        global_address : global_address;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        balance_updates
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address balance_updates r.(consumed_gas) r.(size_of_constant)
          r.(global_address).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        consumed_gas
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address r.(balance_updates) consumed_gas r.(size_of_constant)
          r.(global_address).
      Definition with_size_of_constant
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        size_of_constant
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address r.(balance_updates) r.(consumed_gas) size_of_constant
          r.(global_address).
      Definition with_global_address
        {t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
        global_address
        (r :
          record t_balance_updates t_consumed_gas t_size_of_constant
            t_global_address) :=
        Build t_balance_updates t_consumed_gas t_size_of_constant
          t_global_address r.(balance_updates) r.(consumed_gas)
          r.(size_of_constant) global_address.
    End Register_global_constant_result.
    Definition Register_global_constant_result_skeleton :=
      Register_global_constant_result.record.

    Module Set_deposits_limit_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Set_deposits_limit_result.
    Definition Set_deposits_limit_result_skeleton :=
      Set_deposits_limit_result.record.

    Module Increase_paid_storage_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Increase_paid_storage_result.
    Definition Increase_paid_storage_result_skeleton :=
      Increase_paid_storage_result.record.

    Module Update_consensus_key_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Update_consensus_key_result.
    Definition Update_consensus_key_result_skeleton :=
      Update_consensus_key_result.record.

    Module Tx_rollup_origination_result.
      Record record {balance_updates consumed_gas originated_tx_rollup : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        originated_tx_rollup : originated_tx_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_originated_tx_rollup}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
        Build t_balance_updates t_consumed_gas t_originated_tx_rollup
          balance_updates r.(consumed_gas) r.(originated_tx_rollup).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_originated_tx_rollup} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
        Build t_balance_updates t_consumed_gas t_originated_tx_rollup
          r.(balance_updates) consumed_gas r.(originated_tx_rollup).
      Definition with_originated_tx_rollup
        {t_balance_updates t_consumed_gas t_originated_tx_rollup}
        originated_tx_rollup
        (r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
        Build t_balance_updates t_consumed_gas t_originated_tx_rollup
          r.(balance_updates) r.(consumed_gas) originated_tx_rollup.
    End Tx_rollup_origination_result.
    Definition Tx_rollup_origination_result_skeleton :=
      Tx_rollup_origination_result.record.

    Module Tx_rollup_submit_batch_result.
      Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        paid_storage_size_diff
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Tx_rollup_submit_batch_result.
    Definition Tx_rollup_submit_batch_result_skeleton :=
      Tx_rollup_submit_batch_result.record.

    Module Tx_rollup_commit_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Tx_rollup_commit_result.
    Definition Tx_rollup_commit_result_skeleton :=
      Tx_rollup_commit_result.record.

    Module Tx_rollup_return_bond_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Tx_rollup_return_bond_result.
    Definition Tx_rollup_return_bond_result_skeleton :=
      Tx_rollup_return_bond_result.record.

    Module Tx_rollup_finalize_commitment_result.
      Record record {balance_updates consumed_gas level : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        level : level;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
        balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level balance_updates
          r.(consumed_gas) r.(level).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
        consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          consumed_gas r.(level).
      Definition with_level {t_balance_updates t_consumed_gas t_level} level
        (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          r.(consumed_gas) level.
    End Tx_rollup_finalize_commitment_result.
    Definition Tx_rollup_finalize_commitment_result_skeleton :=
      Tx_rollup_finalize_commitment_result.record.

    Module Tx_rollup_remove_commitment_result.
      Record record {balance_updates consumed_gas level : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        level : level;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
        balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level balance_updates
          r.(consumed_gas) r.(level).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
        consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          consumed_gas r.(level).
      Definition with_level {t_balance_updates t_consumed_gas t_level} level
        (r : record t_balance_updates t_consumed_gas t_level) :=
        Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
          r.(consumed_gas) level.
    End Tx_rollup_remove_commitment_result.
    Definition Tx_rollup_remove_commitment_result_skeleton :=
      Tx_rollup_remove_commitment_result.record.

    Module Tx_rollup_rejection_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Tx_rollup_rejection_result.
    Definition Tx_rollup_rejection_result_skeleton :=
      Tx_rollup_rejection_result.record.

    Module Tx_rollup_dispatch_tickets_result.
      Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        paid_storage_size_diff
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Tx_rollup_dispatch_tickets_result.
    Definition Tx_rollup_dispatch_tickets_result_skeleton :=
      Tx_rollup_dispatch_tickets_result.record.

    Module Transfer_ticket_result.
      Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        paid_storage_size_diff
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Transfer_ticket_result.
    Definition Transfer_ticket_result_skeleton := Transfer_ticket_result.record.

    Module Dal_publish_slot_header_result.
      Record record {consumed_gas : Set} : Set := Build {
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas} consumed_gas
        (r : record t_consumed_gas) :=
        Build t_consumed_gas consumed_gas.
    End Dal_publish_slot_header_result.
    Definition Dal_publish_slot_header_result_skeleton :=
      Dal_publish_slot_header_result.record.

    Module Sc_rollup_originate_result.
      Record record {balance_updates address genesis_commitment_hash
        consumed_gas size : Set} : Set := Build {
        balance_updates : balance_updates;
        address : address;
        genesis_commitment_hash : genesis_commitment_hash;
        consumed_gas : consumed_gas;
        size : size;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
          t_size} balance_updates
        (r :
          record t_balance_updates t_address t_genesis_commitment_hash
            t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_genesis_commitment_hash
          t_consumed_gas t_size balance_updates r.(address)
          r.(genesis_commitment_hash) r.(consumed_gas) r.(size).
      Definition with_address
        {t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
          t_size} address
        (r :
          record t_balance_updates t_address t_genesis_commitment_hash
            t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_genesis_commitment_hash
          t_consumed_gas t_size r.(balance_updates) address
          r.(genesis_commitment_hash) r.(consumed_gas) r.(size).
      Definition with_genesis_commitment_hash
        {t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
          t_size} genesis_commitment_hash
        (r :
          record t_balance_updates t_address t_genesis_commitment_hash
            t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_genesis_commitment_hash
          t_consumed_gas t_size r.(balance_updates) r.(address)
          genesis_commitment_hash r.(consumed_gas) r.(size).
      Definition with_consumed_gas
        {t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
          t_size} consumed_gas
        (r :
          record t_balance_updates t_address t_genesis_commitment_hash
            t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_genesis_commitment_hash
          t_consumed_gas t_size r.(balance_updates) r.(address)
          r.(genesis_commitment_hash) consumed_gas r.(size).
      Definition with_size
        {t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
          t_size} size
        (r :
          record t_balance_updates t_address t_genesis_commitment_hash
            t_consumed_gas t_size) :=
        Build t_balance_updates t_address t_genesis_commitment_hash
          t_consumed_gas t_size r.(balance_updates) r.(address)
          r.(genesis_commitment_hash) r.(consumed_gas) size.
    End Sc_rollup_originate_result.
    Definition Sc_rollup_originate_result_skeleton :=
      Sc_rollup_originate_result.record.

    Module Sc_rollup_add_messages_result.
      Record record {consumed_gas inbox_after : Set} : Set := Build {
        consumed_gas : consumed_gas;
        inbox_after : inbox_after;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas t_inbox_after} consumed_gas
        (r : record t_consumed_gas t_inbox_after) :=
        Build t_consumed_gas t_inbox_after consumed_gas r.(inbox_after).
      Definition with_inbox_after {t_consumed_gas t_inbox_after} inbox_after
        (r : record t_consumed_gas t_inbox_after) :=
        Build t_consumed_gas t_inbox_after r.(consumed_gas) inbox_after.
    End Sc_rollup_add_messages_result.
    Definition Sc_rollup_add_messages_result_skeleton :=
      Sc_rollup_add_messages_result.record.

    Module Sc_rollup_cement_result.
      Record record {consumed_gas inbox_level : Set} : Set := Build {
        consumed_gas : consumed_gas;
        inbox_level : inbox_level;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas {t_consumed_gas t_inbox_level} consumed_gas
        (r : record t_consumed_gas t_inbox_level) :=
        Build t_consumed_gas t_inbox_level consumed_gas r.(inbox_level).
      Definition with_inbox_level {t_consumed_gas t_inbox_level} inbox_level
        (r : record t_consumed_gas t_inbox_level) :=
        Build t_consumed_gas t_inbox_level r.(consumed_gas) inbox_level.
    End Sc_rollup_cement_result.
    Definition Sc_rollup_cement_result_skeleton :=
      Sc_rollup_cement_result.record.

    Module Sc_rollup_publish_result.
      Record record {consumed_gas staked_hash published_at_level balance_updates
        : Set} : Set := Build {
        consumed_gas : consumed_gas;
        staked_hash : staked_hash;
        published_at_level : published_at_level;
        balance_updates : balance_updates;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas
        {t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
        consumed_gas
        (r :
          record t_consumed_gas t_staked_hash t_published_at_level
            t_balance_updates) :=
        Build t_consumed_gas t_staked_hash t_published_at_level
          t_balance_updates consumed_gas r.(staked_hash) r.(published_at_level)
          r.(balance_updates).
      Definition with_staked_hash
        {t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
        staked_hash
        (r :
          record t_consumed_gas t_staked_hash t_published_at_level
            t_balance_updates) :=
        Build t_consumed_gas t_staked_hash t_published_at_level
          t_balance_updates r.(consumed_gas) staked_hash r.(published_at_level)
          r.(balance_updates).
      Definition with_published_at_level
        {t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
        published_at_level
        (r :
          record t_consumed_gas t_staked_hash t_published_at_level
            t_balance_updates) :=
        Build t_consumed_gas t_staked_hash t_published_at_level
          t_balance_updates r.(consumed_gas) r.(staked_hash) published_at_level
          r.(balance_updates).
      Definition with_balance_updates
        {t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
        balance_updates
        (r :
          record t_consumed_gas t_staked_hash t_published_at_level
            t_balance_updates) :=
        Build t_consumed_gas t_staked_hash t_published_at_level
          t_balance_updates r.(consumed_gas) r.(staked_hash)
          r.(published_at_level) balance_updates.
    End Sc_rollup_publish_result.
    Definition Sc_rollup_publish_result_skeleton :=
      Sc_rollup_publish_result.record.

    Module Sc_rollup_refute_result.
      Record record {consumed_gas game_status balance_updates : Set} : Set := Build {
        consumed_gas : consumed_gas;
        game_status : game_status;
        balance_updates : balance_updates;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas
        {t_consumed_gas t_game_status t_balance_updates} consumed_gas
        (r : record t_consumed_gas t_game_status t_balance_updates) :=
        Build t_consumed_gas t_game_status t_balance_updates consumed_gas
          r.(game_status) r.(balance_updates).
      Definition with_game_status
        {t_consumed_gas t_game_status t_balance_updates} game_status
        (r : record t_consumed_gas t_game_status t_balance_updates) :=
        Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
          game_status r.(balance_updates).
      Definition with_balance_updates
        {t_consumed_gas t_game_status t_balance_updates} balance_updates
        (r : record t_consumed_gas t_game_status t_balance_updates) :=
        Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
          r.(game_status) balance_updates.
    End Sc_rollup_refute_result.
    Definition Sc_rollup_refute_result_skeleton :=
      Sc_rollup_refute_result.record.

    Module Sc_rollup_timeout_result.
      Record record {consumed_gas game_status balance_updates : Set} : Set := Build {
        consumed_gas : consumed_gas;
        game_status : game_status;
        balance_updates : balance_updates;
      }.
      Arguments record : clear implicits.
      Definition with_consumed_gas
        {t_consumed_gas t_game_status t_balance_updates} consumed_gas
        (r : record t_consumed_gas t_game_status t_balance_updates) :=
        Build t_consumed_gas t_game_status t_balance_updates consumed_gas
          r.(game_status) r.(balance_updates).
      Definition with_game_status
        {t_consumed_gas t_game_status t_balance_updates} game_status
        (r : record t_consumed_gas t_game_status t_balance_updates) :=
        Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
          game_status r.(balance_updates).
      Definition with_balance_updates
        {t_consumed_gas t_game_status t_balance_updates} balance_updates
        (r : record t_consumed_gas t_game_status t_balance_updates) :=
        Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
          r.(game_status) balance_updates.
    End Sc_rollup_timeout_result.
    Definition Sc_rollup_timeout_result_skeleton :=
      Sc_rollup_timeout_result.record.

    Module Sc_rollup_execute_outbox_message_result.
      Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        paid_storage_size_diff
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Sc_rollup_execute_outbox_message_result.
    Definition Sc_rollup_execute_outbox_message_result_skeleton :=
      Sc_rollup_execute_outbox_message_result.record.

    Module Sc_rollup_recover_bond_result.
      Record record {balance_updates consumed_gas : Set} : Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates {t_balance_updates t_consumed_gas}
        balance_updates (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
      Definition with_consumed_gas {t_balance_updates t_consumed_gas}
        consumed_gas (r : record t_balance_updates t_consumed_gas) :=
        Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
    End Sc_rollup_recover_bond_result.
    Definition Sc_rollup_recover_bond_result_skeleton :=
      Sc_rollup_recover_bond_result.record.

    Module Zk_rollup_origination_result.
      Record record {balance_updates originated_zk_rollup consumed_gas
        storage_size : Set} : Set := Build {
        balance_updates : balance_updates;
        originated_zk_rollup : originated_zk_rollup;
        consumed_gas : consumed_gas;
        storage_size : storage_size;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
        balance_updates
        (r :
          record t_balance_updates t_originated_zk_rollup t_consumed_gas
            t_storage_size) :=
        Build t_balance_updates t_originated_zk_rollup t_consumed_gas
          t_storage_size balance_updates r.(originated_zk_rollup)
          r.(consumed_gas) r.(storage_size).
      Definition with_originated_zk_rollup
        {t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
        originated_zk_rollup
        (r :
          record t_balance_updates t_originated_zk_rollup t_consumed_gas
            t_storage_size) :=
        Build t_balance_updates t_originated_zk_rollup t_consumed_gas
          t_storage_size r.(balance_updates) originated_zk_rollup
          r.(consumed_gas) r.(storage_size).
      Definition with_consumed_gas
        {t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
        consumed_gas
        (r :
          record t_balance_updates t_originated_zk_rollup t_consumed_gas
            t_storage_size) :=
        Build t_balance_updates t_originated_zk_rollup t_consumed_gas
          t_storage_size r.(balance_updates) r.(originated_zk_rollup)
          consumed_gas r.(storage_size).
      Definition with_storage_size
        {t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
        storage_size
        (r :
          record t_balance_updates t_originated_zk_rollup t_consumed_gas
            t_storage_size) :=
        Build t_balance_updates t_originated_zk_rollup t_consumed_gas
          t_storage_size r.(balance_updates) r.(originated_zk_rollup)
          r.(consumed_gas) storage_size.
    End Zk_rollup_origination_result.
    Definition Zk_rollup_origination_result_skeleton :=
      Zk_rollup_origination_result.record.

    Module Zk_rollup_publish_result.
      Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        paid_storage_size_diff
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Zk_rollup_publish_result.
    Definition Zk_rollup_publish_result_skeleton :=
      Zk_rollup_publish_result.record.

    Module Zk_rollup_update_result.
      Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
        Set := Build {
        balance_updates : balance_updates;
        consumed_gas : consumed_gas;
        paid_storage_size_diff : paid_storage_size_diff;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        balance_updates
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
      Definition with_consumed_gas
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
      Definition with_paid_storage_size_diff
        {t_balance_updates t_consumed_gas t_paid_storage_size_diff}
        paid_storage_size_diff
        (r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
        Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
          r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
    End Zk_rollup_update_result.
    Definition Zk_rollup_update_result_skeleton :=
      Zk_rollup_update_result.record.
  End successful_manager_operation_result.
End ConstructorRecords_successful_manager_operation_result.
Import ConstructorRecords_successful_manager_operation_result.

Reserved Notation "'successful_manager_operation_result.Reveal_result".
Reserved Notation "'successful_manager_operation_result.Delegation_result".
Reserved Notation
  "'successful_manager_operation_result.Register_global_constant_result".
Reserved Notation
  "'successful_manager_operation_result.Set_deposits_limit_result".
Reserved Notation
  "'successful_manager_operation_result.Increase_paid_storage_result".
Reserved Notation
  "'successful_manager_operation_result.Update_consensus_key_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_origination_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_submit_batch_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_commit_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_return_bond_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_finalize_commitment_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_remove_commitment_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_rejection_result".
Reserved Notation
  "'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result".
Reserved Notation "'successful_manager_operation_result.Transfer_ticket_result".
Reserved Notation
  "'successful_manager_operation_result.Dal_publish_slot_header_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_originate_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_add_messages_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_cement_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_publish_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_refute_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_timeout_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result".
Reserved Notation
  "'successful_manager_operation_result.Sc_rollup_recover_bond_result".
Reserved Notation
  "'successful_manager_operation_result.Zk_rollup_origination_result".
Reserved Notation
  "'successful_manager_operation_result.Zk_rollup_publish_result".
Reserved Notation
  "'successful_manager_operation_result.Zk_rollup_update_result".

Inductive successful_manager_operation_result : Set :=
| Reveal_result :
  'successful_manager_operation_result.Reveal_result →
  successful_manager_operation_result
| Transaction_result :
  successful_transaction_result → successful_manager_operation_result
| Origination_result :
  successful_origination_result → successful_manager_operation_result
| Delegation_result :
  'successful_manager_operation_result.Delegation_result →
  successful_manager_operation_result
| Register_global_constant_result :
  'successful_manager_operation_result.Register_global_constant_result →
  successful_manager_operation_result
| Set_deposits_limit_result :
  'successful_manager_operation_result.Set_deposits_limit_result →
  successful_manager_operation_result
| Increase_paid_storage_result :
  'successful_manager_operation_result.Increase_paid_storage_result →
  successful_manager_operation_result
| Update_consensus_key_result :
  'successful_manager_operation_result.Update_consensus_key_result →
  successful_manager_operation_result
| Tx_rollup_origination_result :
  'successful_manager_operation_result.Tx_rollup_origination_result →
  successful_manager_operation_result
| Tx_rollup_submit_batch_result :
  'successful_manager_operation_result.Tx_rollup_submit_batch_result →
  successful_manager_operation_result
| Tx_rollup_commit_result :
  'successful_manager_operation_result.Tx_rollup_commit_result →
  successful_manager_operation_result
| Tx_rollup_return_bond_result :
  'successful_manager_operation_result.Tx_rollup_return_bond_result →
  successful_manager_operation_result
| Tx_rollup_finalize_commitment_result :
  'successful_manager_operation_result.Tx_rollup_finalize_commitment_result →
  successful_manager_operation_result
| Tx_rollup_remove_commitment_result :
  'successful_manager_operation_result.Tx_rollup_remove_commitment_result →
  successful_manager_operation_result
| Tx_rollup_rejection_result :
  'successful_manager_operation_result.Tx_rollup_rejection_result →
  successful_manager_operation_result
| Tx_rollup_dispatch_tickets_result :
  'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result →
  successful_manager_operation_result
| Transfer_ticket_result :
  'successful_manager_operation_result.Transfer_ticket_result →
  successful_manager_operation_result
| Dal_publish_slot_header_result :
  'successful_manager_operation_result.Dal_publish_slot_header_result →
  successful_manager_operation_result
| Sc_rollup_originate_result :
  'successful_manager_operation_result.Sc_rollup_originate_result →
  successful_manager_operation_result
| Sc_rollup_add_messages_result :
  'successful_manager_operation_result.Sc_rollup_add_messages_result →
  successful_manager_operation_result
| Sc_rollup_cement_result :
  'successful_manager_operation_result.Sc_rollup_cement_result →
  successful_manager_operation_result
| Sc_rollup_publish_result :
  'successful_manager_operation_result.Sc_rollup_publish_result →
  successful_manager_operation_result
| Sc_rollup_refute_result :
  'successful_manager_operation_result.Sc_rollup_refute_result →
  successful_manager_operation_result
| Sc_rollup_timeout_result :
  'successful_manager_operation_result.Sc_rollup_timeout_result →
  successful_manager_operation_result
| Sc_rollup_execute_outbox_message_result :
  'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result
  → successful_manager_operation_result
| Sc_rollup_recover_bond_result :
  'successful_manager_operation_result.Sc_rollup_recover_bond_result →
  successful_manager_operation_result
| Zk_rollup_origination_result :
  'successful_manager_operation_result.Zk_rollup_origination_result →
  successful_manager_operation_result
| Zk_rollup_publish_result :
  'successful_manager_operation_result.Zk_rollup_publish_result →
  successful_manager_operation_result
| Zk_rollup_update_result :
  'successful_manager_operation_result.Zk_rollup_update_result →
  successful_manager_operation_result

where "'successful_manager_operation_result.Reveal_result" :=
  (successful_manager_operation_result.Reveal_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Delegation_result" :=
  (successful_manager_operation_result.Delegation_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Register_global_constant_result" :=
  (successful_manager_operation_result.Register_global_constant_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t
    Script_expr_hash.t)
and "'successful_manager_operation_result.Set_deposits_limit_result" :=
  (successful_manager_operation_result.Set_deposits_limit_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Increase_paid_storage_result" :=
  (successful_manager_operation_result.Increase_paid_storage_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Update_consensus_key_result" :=
  (successful_manager_operation_result.Update_consensus_key_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_origination_result" :=
  (successful_manager_operation_result.Tx_rollup_origination_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
    Alpha_context.Tx_rollup.t)
and "'successful_manager_operation_result.Tx_rollup_submit_batch_result" :=
  (successful_manager_operation_result.Tx_rollup_submit_batch_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Tx_rollup_commit_result" :=
  (successful_manager_operation_result.Tx_rollup_commit_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_return_bond_result" :=
  (successful_manager_operation_result.Tx_rollup_return_bond_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_finalize_commitment_result"
  :=
  (successful_manager_operation_result.Tx_rollup_finalize_commitment_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
    Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_remove_commitment_result" :=
  (successful_manager_operation_result.Tx_rollup_remove_commitment_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
    Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_rejection_result" :=
  (successful_manager_operation_result.Tx_rollup_rejection_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result" :=
  (successful_manager_operation_result.Tx_rollup_dispatch_tickets_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Transfer_ticket_result" :=
  (successful_manager_operation_result.Transfer_ticket_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Dal_publish_slot_header_result" :=
  (successful_manager_operation_result.Dal_publish_slot_header_result_skeleton
    Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Sc_rollup_originate_result" :=
  (successful_manager_operation_result.Sc_rollup_originate_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Sc_rollup.Address.t
    Alpha_context.Sc_rollup.Commitment.Hash.t Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_add_messages_result" :=
  (successful_manager_operation_result.Sc_rollup_add_messages_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Inbox.t)
and "'successful_manager_operation_result.Sc_rollup_cement_result" :=
  (successful_manager_operation_result.Sc_rollup_cement_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Raw_level.t)
and "'successful_manager_operation_result.Sc_rollup_publish_result" :=
  (successful_manager_operation_result.Sc_rollup_publish_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Commitment.Hash.t
    Alpha_context.Raw_level.t Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_refute_result" :=
  (successful_manager_operation_result.Sc_rollup_refute_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Game.status
    Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_timeout_result" :=
  (successful_manager_operation_result.Sc_rollup_timeout_result_skeleton
    Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Game.status
    Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result"
  :=
  (successful_manager_operation_result.Sc_rollup_execute_outbox_message_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_recover_bond_result" :=
  (successful_manager_operation_result.Sc_rollup_recover_bond_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Zk_rollup_origination_result" :=
  (successful_manager_operation_result.Zk_rollup_origination_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Zk_rollup.t
    Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Zk_rollup_publish_result" :=
  (successful_manager_operation_result.Zk_rollup_publish_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Zk_rollup_update_result" :=
  (successful_manager_operation_result.Zk_rollup_update_result_skeleton
    Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t).

Module successful_manager_operation_result.
  Include ConstructorRecords_successful_manager_operation_result.successful_manager_operation_result.
  Definition Reveal_result :=
    'successful_manager_operation_result.Reveal_result.
  Definition Delegation_result :=
    'successful_manager_operation_result.Delegation_result.
  Definition Register_global_constant_result :=
    'successful_manager_operation_result.Register_global_constant_result.
  Definition Set_deposits_limit_result :=
    'successful_manager_operation_result.Set_deposits_limit_result.
  Definition Increase_paid_storage_result :=
    'successful_manager_operation_result.Increase_paid_storage_result.
  Definition Update_consensus_key_result :=
    'successful_manager_operation_result.Update_consensus_key_result.
  Definition Tx_rollup_origination_result :=
    'successful_manager_operation_result.Tx_rollup_origination_result.
  Definition Tx_rollup_submit_batch_result :=
    'successful_manager_operation_result.Tx_rollup_submit_batch_result.
  Definition Tx_rollup_commit_result :=
    'successful_manager_operation_result.Tx_rollup_commit_result.
  Definition Tx_rollup_return_bond_result :=
    'successful_manager_operation_result.Tx_rollup_return_bond_result.
  Definition Tx_rollup_finalize_commitment_result :=
    'successful_manager_operation_result.Tx_rollup_finalize_commitment_result.
  Definition Tx_rollup_remove_commitment_result :=
    'successful_manager_operation_result.Tx_rollup_remove_commitment_result.
  Definition Tx_rollup_rejection_result :=
    'successful_manager_operation_result.Tx_rollup_rejection_result.
  Definition Tx_rollup_dispatch_tickets_result :=
    'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.
  Definition Transfer_ticket_result :=
    'successful_manager_operation_result.Transfer_ticket_result.
  Definition Dal_publish_slot_header_result :=
    'successful_manager_operation_result.Dal_publish_slot_header_result.
  Definition Sc_rollup_originate_result :=
    'successful_manager_operation_result.Sc_rollup_originate_result.
  Definition Sc_rollup_add_messages_result :=
    'successful_manager_operation_result.Sc_rollup_add_messages_result.
  Definition Sc_rollup_cement_result :=
    'successful_manager_operation_result.Sc_rollup_cement_result.
  Definition Sc_rollup_publish_result :=
    'successful_manager_operation_result.Sc_rollup_publish_result.
  Definition Sc_rollup_refute_result :=
    'successful_manager_operation_result.Sc_rollup_refute_result.
  Definition Sc_rollup_timeout_result :=
    'successful_manager_operation_result.Sc_rollup_timeout_result.
  Definition Sc_rollup_execute_outbox_message_result :=
    'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.
  Definition Sc_rollup_recover_bond_result :=
    'successful_manager_operation_result.Sc_rollup_recover_bond_result.
  Definition Zk_rollup_origination_result :=
    'successful_manager_operation_result.Zk_rollup_origination_result.
  Definition Zk_rollup_publish_result :=
    'successful_manager_operation_result.Zk_rollup_publish_result.
  Definition Zk_rollup_update_result :=
    'successful_manager_operation_result.Zk_rollup_update_result.
End successful_manager_operation_result.

Definition migration_origination_result_to_successful_manager_operation_result
  (function_parameter : Alpha_context.Migration.origination_result)
  : successful_manager_operation_result :=
  let '{|
    Alpha_context.Migration.origination_result.balance_updates := balance_updates;
      Alpha_context.Migration.origination_result.originated_contracts :=
        originated_contracts;
      Alpha_context.Migration.origination_result.storage_size := storage_size;
      Alpha_context.Migration.origination_result.paid_storage_size_diff :=
        paid_storage_size_diff
      |} := function_parameter in
  Origination_result
    {|
      Apply_internal_results.successful_origination_result.lazy_storage_diff :=
        None;
      Apply_internal_results.successful_origination_result.balance_updates :=
        balance_updates;
      Apply_internal_results.successful_origination_result.originated_contracts
        := originated_contracts;
      Apply_internal_results.successful_origination_result.consumed_gas :=
        Alpha_context.Gas.Arith.zero;
      Apply_internal_results.successful_origination_result.storage_size :=
        storage_size;
      Apply_internal_results.successful_origination_result.paid_storage_size_diff
        := paid_storage_size_diff; |}.

Inductive packed_successful_manager_operation_result : Set :=
| Successful_manager_result :
  successful_manager_operation_result →
  packed_successful_manager_operation_result.

Definition pack_migration_operation_results
  (results : list Alpha_context.Migration.origination_result)
  : list packed_successful_manager_operation_result :=
  List.map
    (fun (el : Alpha_context.Migration.origination_result) ⇒
      Successful_manager_result
        (migration_origination_result_to_successful_manager_operation_result el))
    results.

Definition manager_operation_result : Set :=
  Apply_operation_result.operation_result Alpha_context.Kind.manager
    successful_manager_operation_result.

Module Manager_result.

Records for the constructor parameters

  Module ConstructorRecords_case.
    Module case.
      Module MCase.
        Record record {op_case encoding kind select proj inj t : Set} : Set := Build {
          op_case : op_case;
          encoding : encoding;
          kind : kind;
          select : select;
          proj : proj;
          inj : inj;
          t : t;
        }.
        Arguments record : clear implicits.
        Definition with_op_case
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} op_case
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t op_case
            r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) r.(t).
        Definition with_encoding
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} encoding
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) encoding r.(kind) r.(select) r.(proj) r.(inj) r.(t).
        Definition with_kind
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} kind
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) kind r.(select) r.(proj) r.(inj) r.(t).
        Definition with_select
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} select
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) select r.(proj) r.(inj) r.(t).
        Definition with_proj
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} proj
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) r.(select) proj r.(inj) r.(t).
        Definition with_inj
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} inj
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) inj r.(t).
        Definition with_t
          {t_op_case t_encoding t_kind t_select t_proj t_inj t_t} t
          (r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
          Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
            r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) t.
      End MCase.
      Definition MCase_skeleton := MCase.record.
    End case.
  End ConstructorRecords_case.
  Import ConstructorRecords_case.

  Reserved Notation "'case.MCase".

  Inductive case (kind : Set) : Set :=
  | MCase : ∀ {a : Set}, 'case.MCase a → case kind
  
  where "'case.MCase" :=
    (fun (t_a : Set) ⇒ case.MCase_skeleton
      Alpha_context.Operation.Encoding.Manager_operations.case
      (Data_encoding.t t_a) Alpha_context.Kind.manager
      (packed_successful_manager_operation_result →
      option successful_manager_operation_result)
      (successful_manager_operation_result → t_a)
      (t_a → successful_manager_operation_result)
      (Data_encoding.t manager_operation_result)).

  Module case.
    Include ConstructorRecords_case.case.
    Definition MCase := 'case.MCase.
  End case.

  Arguments MCase {_ _}.

  Definition make {A B : Set}
    (op_case : Alpha_context.Operation.Encoding.Manager_operations.case)
    (encoding : Data_encoding.encoding A)
    (kind_value : Alpha_context.Kind.manager)
    (select :
      packed_successful_manager_operation_result →
      option successful_manager_operation_result)
    (proj : successful_manager_operation_result → A)
    (inj : A → successful_manager_operation_result) : case B :=
    let
      'Alpha_context.Operation.Encoding.Manager_operations.MCase {|
        Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name := name
          |} := op_case in
    let t_value :=
      Data_encoding.def
        (Format.asprintf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal
              "operation.alpha.operation_result."
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format))
            "operation.alpha.operation_result.%s") name) None None
        (Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
          [
            Data_encoding.case_value "Applied" None (Data_encoding.Tag 0)
              (Data_encoding.merge_objs
                (Data_encoding.obj1
                  (Data_encoding.req None None "status"
                    (Data_encoding.constant
                      "applied")))
                encoding)
              (fun (o_value :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_manager_operation_result)
                ⇒
                match o_value with
                |
                  (Apply_operation_result.Skipped _ |
                  Apply_operation_result.Failed _ _ |
                  Apply_operation_result.Backtracked _ _)
                  ⇒ None
                | Apply_operation_result.Applied o_value ⇒
                  let o_value :=
                    cast
                      successful_manager_operation_result
                      o_value in
                  match
                    select
                      (Successful_manager_result
                        o_value)
                    with
                  | None ⇒ None
                  | Some o_value ⇒
                    Some (tt, (proj o_value))
                  end
                end)
              (fun (function_parameter : unit × A) ⇒
                let '(_, x_value) := function_parameter in
                Apply_operation_result.Applied (inj x_value));
            Data_encoding.case_value "Failed" None (Data_encoding.Tag 1)
              (Data_encoding.obj2
                (Data_encoding.req None None "status"
                  (Data_encoding.constant "failed"))
                (Data_encoding.req None None "errors"
                  Apply_operation_result.trace_encoding))
              (fun (function_parameter :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_manager_operation_result)
                ⇒
                match function_parameter with
                | Apply_operation_result.Failed _ errs ⇒
                  Some (tt, errs)
                | _ ⇒ None
                end)
              (fun (function_parameter :
                unit × Error_monad.trace Error_monad._error) ⇒
                let '(_, errs) := function_parameter in
                Apply_operation_result.Failed kind_value errs);
            Data_encoding.case_value "Skipped" None (Data_encoding.Tag 2)
              (Data_encoding.obj1
                (Data_encoding.req None None "status"
                  (Data_encoding.constant "skipped")))
              (fun (function_parameter :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_manager_operation_result)
                ⇒
                match function_parameter with
                | Apply_operation_result.Skipped _ ⇒ Some tt
                | _ ⇒ None
                end)
              (fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                Apply_operation_result.Skipped kind_value);
            Data_encoding.case_value "Backtracked" None (Data_encoding.Tag 3)
              (Data_encoding.merge_objs
                (Data_encoding.obj2
                  (Data_encoding.req None None "status"
                    (Data_encoding.constant
                      "backtracked"))
                  (Data_encoding.opt None None "errors"
                    Apply_operation_result.trace_encoding))
                encoding)
              (fun (o_value :
                Apply_operation_result.operation_result
                  Alpha_context.Kind.manager
                  successful_manager_operation_result)
                ⇒
                match o_value with
                |
                  (Apply_operation_result.Skipped _ |
                  Apply_operation_result.Failed _ _ |
                  Apply_operation_result.Applied _) ⇒
                  None
                |
                  Apply_operation_result.Backtracked
                    o_value errs ⇒
                  let '[errs, o_value] :=
                    cast
                      [option
                        (Error_monad.trace
                          Error_monad._error)
                        **
                        successful_manager_operation_result]
                      [errs, o_value] in
                  match
                    select
                      (Successful_manager_result
                        o_value)
                    with
                  | None ⇒ None
                  | Some o_value ⇒
                    Some
                      ((tt, errs),
                        (proj
                          o_value))
                  end
                end)
              (fun (function_parameter :
                (unit ×
                  option
                    (Error_monad.trace
                      Error_monad._error))
                  × A) ⇒
                let '((_, errs), x_value) := function_parameter
                  in
                Apply_operation_result.Backtracked (inj x_value)
                  errs)
          ]) in
    MCase
      {| case.MCase.op_case := op_case; case.MCase.encoding := encoding;
        case.MCase.kind := kind_value; case.MCase.select := select;
        case.MCase.proj := proj; case.MCase.inj := inj; case.MCase.t := t_value;
        |}.

  Definition reveal_case : case Alpha_context.Kind.reveal :=
    make Alpha_context.Operation.Encoding.Manager_operations.reveal_case
      (Data_encoding.obj1
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Reveal_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Reveal_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Reveal_result {|
            successful_manager_operation_result.Reveal_result.consumed_gas := consumed_gas
              |} ⇒ consumed_gas
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        Reveal_result
          {|
            successful_manager_operation_result.Reveal_result.consumed_gas :=
              consumed_gas; |}).

  Definition transaction_contract_variant_cases
    : Data_encoding.encoding
      Apply_internal_results.successful_transaction_result :=
    Data_encoding.union None
      [
        Data_encoding.case_value "To_contract" None (Data_encoding.Tag 0)
          (Data_encoding.obj9
            (Data_encoding.opt None None "storage"
              Alpha_context.Script.expr_encoding)
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.dft None None "ticket_updates"
              Ticket_receipt.encoding nil)
            (Data_encoding.dft None None "originated_contracts"
              (Data_encoding.list_value None
                Alpha_context.Contract.originated_encoding) nil)
            (Data_encoding.dft None None "consumed_milligas"
              Alpha_context.Gas.Arith.n_fp_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.dft None None "storage_size"
              Data_encoding.z_value Z.zero)
            (Data_encoding.dft None None "paid_storage_size_diff"
              Data_encoding.z_value Z.zero)
            (Data_encoding.dft None None
              "allocated_destination_contract"
              Data_encoding.bool_value false)
            (Data_encoding.opt None None "lazy_storage_diff"
              Alpha_context.Lazy_storage.encoding))
          (fun (function_parameter :
            Apply_internal_results.successful_transaction_result) ⇒
            match function_parameter with
            |
              Apply_internal_results.Transaction_to_contract_result
                {|
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
                  := storage_value;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
                    :=
                    lazy_storage_diff;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
                    :=
                    balance_updates;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
                    :=
                    ticket_receipt;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
                    :=
                    originated_contracts;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
                    :=
                    consumed_gas;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
                    :=
                    storage_size;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
                    :=
                    paid_storage_size_diff;
                  Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
                    :=
                    allocated_destination_contract
                  |} ⇒
              Some
                (storage_value, balance_updates, ticket_receipt,
                  originated_contracts, consumed_gas,
                  storage_size, paid_storage_size_diff,
                  allocated_destination_contract,
                  lazy_storage_diff)
            | _ ⇒ None
            end)
          (fun (function_parameter :
            option Alpha_context.Script.expr ×
              Alpha_context.Receipt.balance_updates ×
              Ticket_receipt.t × list Contract_hash.t ×
              Alpha_context.Gas.Arith.fp × Z.t × Z.t × bool ×
              option Alpha_context.Lazy_storage.diffs) ⇒
            let
              '(storage_value, balance_updates, ticket_receipt,
                originated_contracts, consumed_gas,
                storage_size, paid_storage_size_diff,
                allocated_destination_contract,
                lazy_storage_diff) := function_parameter in
            Apply_internal_results.Transaction_to_contract_result
              {|
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
                  := storage_value;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
                  := lazy_storage_diff;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
                  := balance_updates;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
                  := ticket_receipt;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
                  := originated_contracts;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
                  := consumed_gas;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
                  := storage_size;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
                  := paid_storage_size_diff;
                Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
                  := allocated_destination_contract; |});
        Data_encoding.case_value "To_tx_rollup" None (Data_encoding.Tag 1)
          (Data_encoding.obj4
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.dft None None "consumed_milligas"
              Alpha_context.Gas.Arith.n_fp_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.req None None "ticket_hash"
              Alpha_context.Ticket_hash.encoding)
            (Data_encoding.req None None "paid_storage_size_diff"
              Data_encoding.n_value))
          (fun (function_parameter :
            Apply_internal_results.successful_transaction_result) ⇒
            match function_parameter with
            |
              Apply_internal_results.Transaction_to_tx_rollup_result
                {|
                Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
                  := ticket_hash;
                  Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
                    :=
                    balance_updates;
                  Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
                    :=
                    consumed_gas;
                  Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
                    :=
                    paid_storage_size_diff
                  |} ⇒
              Some
                (balance_updates, consumed_gas, ticket_hash,
                  paid_storage_size_diff)
            | _ ⇒ None
            end)
          (fun (function_parameter :
            Alpha_context.Receipt.balance_updates ×
              Alpha_context.Gas.Arith.fp ×
              Alpha_context.Ticket_hash.t × Z.t) ⇒
            let
              '(balance_updates, consumed_gas, ticket_hash,
                paid_storage_size_diff) := function_parameter in
            Apply_internal_results.Transaction_to_tx_rollup_result
              {|
                Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
                  := ticket_hash;
                Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
                  := balance_updates;
                Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
                  := consumed_gas;
                Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
                  := paid_storage_size_diff; |});
        Data_encoding.case_value "To_sc_rollup" None (Data_encoding.Tag 2)
          (Data_encoding.obj2
            (Data_encoding.dft None None "consumed_milligas"
              Alpha_context.Gas.Arith.n_fp_encoding
              Alpha_context.Gas.Arith.zero)
            (Data_encoding.req None None "inbox_after"
              Alpha_context.Sc_rollup.Inbox.encoding))
          (fun (function_parameter :
            Apply_internal_results.successful_transaction_result) ⇒
            match function_parameter with
            |
              Apply_internal_results.Transaction_to_sc_rollup_result
                {|
                Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
                  := consumed_gas;
                  Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
                    :=
                    inbox_after
                  |} ⇒ Some (consumed_gas, inbox_after)
            | _ ⇒ None
            end)
          (fun (function_parameter :
            Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t)
            ⇒
            let '(consumed_gas, inbox_after) := function_parameter in
            Apply_internal_results.Transaction_to_sc_rollup_result
              {|
                Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
                  := consumed_gas;
                Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
                  := inbox_after; |})
      ].

  Definition transaction_case : case Alpha_context.Kind.transaction :=
    make Alpha_context.Operation.Encoding.Manager_operations.transaction_case
      transaction_contract_variant_cases
      Alpha_context.Kind.Transaction_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Transaction_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        | Transaction_result x_value ⇒ x_value
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (x_value : Apply_internal_results.successful_transaction_result) ⇒
        Transaction_result x_value).

  Definition origination_case : case Alpha_context.Kind.origination :=
    make Alpha_context.Operation.Encoding.Manager_operations.origination_case
      (Data_encoding.obj6
        (Data_encoding.dft None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding nil)
        (Data_encoding.dft None None "originated_contracts"
          (Data_encoding.list_value None
            Alpha_context.Contract.originated_encoding) nil)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero)
        (Data_encoding.opt None None "lazy_storage_diff"
          Alpha_context.Lazy_storage.encoding))
      Alpha_context.Kind.Origination_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Origination_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Origination_result {|
            Apply_internal_results.successful_origination_result.lazy_storage_diff :=
              lazy_storage_diff;
              Apply_internal_results.successful_origination_result.balance_updates
                := balance_updates;
              Apply_internal_results.successful_origination_result.originated_contracts
                := originated_contracts;
              Apply_internal_results.successful_origination_result.consumed_gas
                := consumed_gas;
              Apply_internal_results.successful_origination_result.storage_size
                := storage_size;
              Apply_internal_results.successful_origination_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒
          (balance_updates, originated_contracts, consumed_gas, storage_size,
            paid_storage_size_diff, lazy_storage_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × list Contract_hash.t ×
          Alpha_context.Gas.Arith.fp × Z.t × Z.t ×
          option Alpha_context.Lazy_storage.diffs) ⇒
        let
          '(balance_updates, originated_contracts, consumed_gas, storage_size,
            paid_storage_size_diff, lazy_storage_diff) := function_parameter in
        Origination_result
          {|
            Apply_internal_results.successful_origination_result.lazy_storage_diff
              := lazy_storage_diff;
            Apply_internal_results.successful_origination_result.balance_updates
              := balance_updates;
            Apply_internal_results.successful_origination_result.originated_contracts
              := originated_contracts;
            Apply_internal_results.successful_origination_result.consumed_gas :=
              consumed_gas;
            Apply_internal_results.successful_origination_result.storage_size :=
              storage_size;
            Apply_internal_results.successful_origination_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition register_global_constant_case
    : case Alpha_context.Kind.register_global_constant :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.register_global_constant_case
      (Data_encoding.obj4
        (Data_encoding.dft None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding nil)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
        (Data_encoding.req None None "global_address" Script_expr_hash.encoding))
      Alpha_context.Kind.Register_global_constant_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Register_global_constant_result _) as op)
          ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Register_global_constant_result {|
            successful_manager_operation_result.Register_global_constant_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Register_global_constant_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Register_global_constant_result.size_of_constant
                := size_of_constant;
              successful_manager_operation_result.Register_global_constant_result.global_address
                := global_address
              |} ⇒
          (balance_updates, consumed_gas, size_of_constant, global_address)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t
          × Script_expr_hash.t) ⇒
        let
          '(balance_updates, consumed_gas, size_of_constant, global_address) :=
          function_parameter in
        Register_global_constant_result
          {|
            successful_manager_operation_result.Register_global_constant_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Register_global_constant_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Register_global_constant_result.size_of_constant
              := size_of_constant;
            successful_manager_operation_result.Register_global_constant_result.global_address
              := global_address; |}).

  Definition delegation_case : case Alpha_context.Kind.delegation :=
    make Alpha_context.Operation.Encoding.Manager_operations.delegation_case
      (Data_encoding.obj1
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Delegation_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Delegation_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Delegation_result {|
            successful_manager_operation_result.Delegation_result.consumed_gas :=
              consumed_gas
              |} ⇒ consumed_gas
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        Delegation_result
          {|
            successful_manager_operation_result.Delegation_result.consumed_gas
              := consumed_gas; |}).

  Definition update_consensus_key_case
    : case Alpha_context.Kind.update_consensus_key :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.update_consensus_key_case
      (Data_encoding.obj1
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Update_consensus_key_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Update_consensus_key_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Update_consensus_key_result {|
            successful_manager_operation_result.Update_consensus_key_result.consumed_gas
              := consumed_gas
              |} ⇒ consumed_gas
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        Update_consensus_key_result
          {|
            successful_manager_operation_result.Update_consensus_key_result.consumed_gas
              := consumed_gas; |}).

  Definition set_deposits_limit_case
    : case Alpha_context.Kind.set_deposits_limit :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.set_deposits_limit_case
      (Data_encoding.obj1
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Set_deposits_limit_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Set_deposits_limit_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Set_deposits_limit_result {|
            successful_manager_operation_result.Set_deposits_limit_result.consumed_gas :=
              consumed_gas
              |} ⇒ consumed_gas
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        Set_deposits_limit_result
          {|
            successful_manager_operation_result.Set_deposits_limit_result.consumed_gas
              := consumed_gas; |}).

  Definition increase_paid_storage_case
    : case Alpha_context.Kind.increase_paid_storage :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.increase_paid_storage_case
      (Data_encoding.obj2
        (Data_encoding.dft None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding nil)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Increase_paid_storage_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Increase_paid_storage_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Increase_paid_storage_result {|
            successful_manager_operation_result.Increase_paid_storage_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
                := consumed_gas
              |} ⇒ (balance_updates, consumed_gas)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas) := function_parameter in
        Increase_paid_storage_result
          {|
            successful_manager_operation_result.Increase_paid_storage_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
              := consumed_gas; |}).

  Definition tx_rollup_origination_case
    : case Alpha_context.Kind.tx_rollup_origination :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_origination_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "originated_rollup"
          Alpha_context.Tx_rollup.encoding))
      Alpha_context.Kind.Tx_rollup_origination_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_origination_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_origination_result {|
            successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
                := originated_tx_rollup
              |} ⇒ (balance_updates, consumed_gas, originated_tx_rollup)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
          Alpha_context.Tx_rollup.t) ⇒
        let '(balance_updates, consumed_gas, originated_tx_rollup) :=
          function_parameter in
        Tx_rollup_origination_result
          {|
            successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
              := originated_tx_rollup; |}).

  Definition tx_rollup_submit_batch_case
    : case Alpha_context.Kind.tx_rollup_submit_batch :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_submit_batch_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "paid_storage_size_diff"
          Data_encoding.n_value))
      Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_submit_batch_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_submit_batch_result {|
            successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
          function_parameter in
        Tx_rollup_submit_batch_result
          {|
            successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition tx_rollup_commit_case : case Alpha_context.Kind.tx_rollup_commit :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_commit_case
      (Data_encoding.obj2
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Tx_rollup_commit_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_commit_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_commit_result {|
            successful_manager_operation_result.Tx_rollup_commit_result.balance_updates :=
              balance_updates;
              successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
                := consumed_gas
              |} ⇒ (balance_updates, consumed_gas)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas) := function_parameter in
        Tx_rollup_commit_result
          {|
            successful_manager_operation_result.Tx_rollup_commit_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
              := consumed_gas; |}).

  Definition tx_rollup_return_bond_case
    : case Alpha_context.Kind.tx_rollup_return_bond :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_return_bond_case
      (Data_encoding.obj2
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Tx_rollup_return_bond_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_return_bond_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_return_bond_result {|
            successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
                := consumed_gas
              |} ⇒ (balance_updates, consumed_gas)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas) := function_parameter in
        Tx_rollup_return_bond_result
          {|
            successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
              := consumed_gas; |}).

  Definition tx_rollup_finalize_commitment_case
    : case Alpha_context.Kind.tx_rollup_finalize_commitment :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_finalize_commitment_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "level"
          Alpha_context.Tx_rollup_level.encoding))
      Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Tx_rollup_finalize_commitment_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_finalize_commitment_result {|
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
                := level
              |} ⇒ (balance_updates, consumed_gas, level)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
          Alpha_context.Tx_rollup_level.t) ⇒
        let '(balance_updates, consumed_gas, level) := function_parameter in
        Tx_rollup_finalize_commitment_result
          {|
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
              := level; |}).

  Definition tx_rollup_remove_commitment_case
    : case Alpha_context.Kind.tx_rollup_remove_commitment :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_remove_commitment_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "level"
          Alpha_context.Tx_rollup_level.encoding))
      Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Tx_rollup_remove_commitment_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_remove_commitment_result {|
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
                := level
              |} ⇒ (balance_updates, consumed_gas, level)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
          Alpha_context.Tx_rollup_level.t) ⇒
        let '(balance_updates, consumed_gas, level) := function_parameter in
        Tx_rollup_remove_commitment_result
          {|
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
              := level; |}).

  Definition tx_rollup_rejection_case
    : case Alpha_context.Kind.tx_rollup_rejection :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_rejection_case
      (Data_encoding.obj2
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Tx_rollup_rejection_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Tx_rollup_rejection_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_rejection_result {|
            successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
                := consumed_gas
              |} ⇒ (balance_updates, consumed_gas)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas) := function_parameter in
        Tx_rollup_rejection_result
          {|
            successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
              := consumed_gas; |}).

  Definition tx_rollup_dispatch_tickets_case
    : case Alpha_context.Kind.tx_rollup_dispatch_tickets :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_dispatch_tickets_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero))
      Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Tx_rollup_dispatch_tickets_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Tx_rollup_dispatch_tickets_result {|
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
          function_parameter in
        Tx_rollup_dispatch_tickets_result
          {|
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition transfer_ticket_case : case Alpha_context.Kind.transfer_ticket :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.transfer_ticket_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero))
      Alpha_context.Kind.Transfer_ticket_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Transfer_ticket_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Transfer_ticket_result {|
            successful_manager_operation_result.Transfer_ticket_result.balance_updates :=
              balance_updates;
              successful_manager_operation_result.Transfer_ticket_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
          function_parameter in
        Transfer_ticket_result
          {|
            successful_manager_operation_result.Transfer_ticket_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Transfer_ticket_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition dal_publish_slot_header_case
    : case Alpha_context.Kind.dal_publish_slot_header :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.dal_publish_slot_header_case
      (Data_encoding.obj1
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Dal_publish_slot_header_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Dal_publish_slot_header_result _) as op)
          ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Dal_publish_slot_header_result {|
            successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
              := consumed_gas
              |} ⇒ consumed_gas
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
        Dal_publish_slot_header_result
          {|
            successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
              := consumed_gas; |}).

  Definition zk_rollup_origination_case
    : case Alpha_context.Kind.zk_rollup_origination :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_origination_case
      (Data_encoding.obj4
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.req None None "originated_zk_rollup"
          Alpha_context.Zk_rollup.Address.encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "size" Data_encoding.z_value))
      Alpha_context.Kind.Zk_rollup_origination_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Zk_rollup_origination_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Zk_rollup_origination_result {|
            successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
                := originated_zk_rollup;
              successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Zk_rollup_origination_result.storage_size
                := storage_size
              |} ⇒
          (balance_updates, originated_zk_rollup, consumed_gas, storage_size)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates ×
          Alpha_context.Zk_rollup.Address.t × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let
          '(balance_updates, originated_zk_rollup, consumed_gas, storage_size) :=
          function_parameter in
        Zk_rollup_origination_result
          {|
            successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
              := originated_zk_rollup;
            successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Zk_rollup_origination_result.storage_size
              := storage_size; |}).

  Definition zk_rollup_publish_case
    : case Alpha_context.Kind.zk_rollup_publish :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_publish_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "size" Data_encoding.z_value))
      Alpha_context.Kind.Zk_rollup_publish_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Zk_rollup_publish_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Zk_rollup_publish_result {|
            successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
          function_parameter in
        Zk_rollup_publish_result
          {|
            successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition zk_rollup_update_case : case Alpha_context.Kind.zk_rollup_update :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_update_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero))
      Alpha_context.Kind.Zk_rollup_update_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Zk_rollup_update_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Zk_rollup_update_result {|
            successful_manager_operation_result.Zk_rollup_update_result.balance_updates :=
              balance_updates;
              successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
          function_parameter in
        Zk_rollup_update_result
          {|
            successful_manager_operation_result.Zk_rollup_update_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition sc_rollup_originate_case
    : case Alpha_context.Kind.sc_rollup_originate :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_originate_case
      (Data_encoding.obj5
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.req None None "address"
          Alpha_context.Sc_rollup.Address.encoding)
        (Data_encoding.req None None "genesis_commitment_hash"
          Alpha_context.Sc_rollup.Commitment.Hash.encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "size" Data_encoding.z_value))
      Alpha_context.Kind.Sc_rollup_originate_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_originate_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_originate_result {|
            successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Sc_rollup_originate_result.address
                := address;
              successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
                := genesis_commitment_hash;
              successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Sc_rollup_originate_result.size
                := size_value
              |} ⇒
          (balance_updates, address, genesis_commitment_hash, consumed_gas,
            size_value)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates ×
          Alpha_context.Sc_rollup.Address.t ×
          Alpha_context.Sc_rollup.Commitment.Hash.t × Alpha_context.Gas.Arith.fp
          × Z.t) ⇒
        let
          '(balance_updates, address, genesis_commitment_hash, consumed_gas,
            size_value) := function_parameter in
        Sc_rollup_originate_result
          {|
            successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Sc_rollup_originate_result.address
              := address;
            successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
              := genesis_commitment_hash;
            successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_originate_result.size
              := size_value; |}).

  Definition sc_rollup_add_messages_case
    : case Alpha_context.Kind.sc_rollup_add_messages :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_add_messages_case
      (Data_encoding.obj2
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "inbox_after"
          Alpha_context.Sc_rollup.Inbox.encoding))
      Alpha_context.Kind.Sc_rollup_add_messages_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_add_messages_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_add_messages_result {|
            successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
              := consumed_gas;
              successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
                := inbox_after
              |} ⇒ (consumed_gas, inbox_after)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t) ⇒
        let '(consumed_gas, inbox_after) := function_parameter in
        Sc_rollup_add_messages_result
          {|
            successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
              := inbox_after; |}).

  Definition sc_rollup_cement_case : case Alpha_context.Kind.sc_rollup_cement :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_cement_case
      (Data_encoding.obj2
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "inbox_level"
          Alpha_context.Raw_level.encoding))
      Alpha_context.Kind.Sc_rollup_cement_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_cement_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_cement_result {|
            successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas :=
              consumed_gas;
              successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
                := inbox_level
              |} ⇒ (consumed_gas, inbox_level)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.fp × Alpha_context.Raw_level.t) ⇒
        let '(consumed_gas, inbox_level) := function_parameter in
        Sc_rollup_cement_result
          {|
            successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
              := inbox_level; |}).

  Definition sc_rollup_publish_case
    : case Alpha_context.Kind.sc_rollup_publish :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_publish_case
      (Data_encoding.obj4
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "staked_hash"
          Alpha_context.Sc_rollup.Commitment.Hash.encoding)
        (Data_encoding.req None None "published_at_level"
          Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding))
      Alpha_context.Kind.Sc_rollup_publish_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_publish_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_publish_result {|
            successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas :=
              consumed_gas;
              successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
                := staked_hash;
              successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
                := published_at_level;
              successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
                := balance_updates
              |} ⇒
          (consumed_gas, staked_hash, published_at_level, balance_updates)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Commitment.Hash.t ×
          Alpha_context.Raw_level.t × Alpha_context.Receipt.balance_updates) ⇒
        let '(consumed_gas, staked_hash, published_at_level, balance_updates) :=
          function_parameter in
        Sc_rollup_publish_result
          {|
            successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
              := staked_hash;
            successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
              := published_at_level;
            successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
              := balance_updates; |}).

  Definition sc_rollup_refute_case : case Alpha_context.Kind.sc_rollup_refute :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_refute_case
      (Data_encoding.obj3
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "game_status"
          Alpha_context.Sc_rollup.Game.status_encoding)
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding))
      Alpha_context.Kind.Sc_rollup_refute_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_refute_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_refute_result {|
            successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas :=
              consumed_gas;
              successful_manager_operation_result.Sc_rollup_refute_result.game_status
                := game_status;
              successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
                := balance_updates
              |} ⇒ (consumed_gas, game_status, balance_updates)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Game.status ×
          Alpha_context.Receipt.balance_updates) ⇒
        let '(consumed_gas, game_status, balance_updates) := function_parameter
          in
        Sc_rollup_refute_result
          {|
            successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_refute_result.game_status
              := game_status;
            successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
              := balance_updates; |}).

  Definition sc_rollup_timeout_case
    : case Alpha_context.Kind.sc_rollup_timeout :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_timeout_case
      (Data_encoding.obj3
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.req None None "game_status"
          Alpha_context.Sc_rollup.Game.status_encoding)
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding))
      Alpha_context.Kind.Sc_rollup_timeout_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_timeout_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_timeout_result {|
            successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas :=
              consumed_gas;
              successful_manager_operation_result.Sc_rollup_timeout_result.game_status
                := game_status;
              successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
                := balance_updates
              |} ⇒ (consumed_gas, game_status, balance_updates)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Game.status ×
          Alpha_context.Receipt.balance_updates) ⇒
        let '(consumed_gas, game_status, balance_updates) := function_parameter
          in
        Sc_rollup_timeout_result
          {|
            successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_timeout_result.game_status
              := game_status;
            successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
              := balance_updates; |}).

  Definition sc_rollup_execute_outbox_message_case
    : case Alpha_context.Kind.sc_rollup_execute_outbox_message :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_execute_outbox_message_case
      (Data_encoding.obj3
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
        (Data_encoding.dft None None "paid_storage_size_diff"
          Data_encoding.z_value Z.zero))
      Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Successful_manager_result
            ((Sc_rollup_execute_outbox_message_result _) as op) ⇒ Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_execute_outbox_message_result {|
            successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
                := consumed_gas;
              successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
                := paid_storage_size_diff
              |} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
        ⇒
        let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
          function_parameter in
        Sc_rollup_execute_outbox_message_result
          {|
            successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
              := consumed_gas;
            successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

  Definition sc_rollup_recover_bond_case
    : case Alpha_context.Kind.sc_rollup_recover_bond :=
    make
      Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_recover_bond_case
      (Data_encoding.obj2
        (Data_encoding.req None None "balance_updates"
          Alpha_context.Receipt.balance_updates_encoding)
        (Data_encoding.dft None None "consumed_milligas"
          Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
      Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind
      (fun (function_parameter : packed_successful_manager_operation_result) ⇒
        match function_parameter with
        | Successful_manager_result ((Sc_rollup_recover_bond_result _) as op) ⇒
          Some op
        | _ ⇒ None
        end)
      (fun (function_parameter : successful_manager_operation_result) ⇒
        match function_parameter with
        |
          Sc_rollup_recover_bond_result {|
            successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
              := balance_updates;
              successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
                := consumed_gas
              |} ⇒ (balance_updates, consumed_gas)
        | _ ⇒ unreachable_gadt_branch
        end)
      (fun (function_parameter :
        Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
        let '(balance_updates, consumed_gas) := function_parameter in
        Sc_rollup_recover_bond_result
          {|
            successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
              := balance_updates;
            successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
              := consumed_gas; |}).
End Manager_result.

Definition successful_manager_operation_result_encoding
  : Data_encoding.t packed_successful_manager_operation_result :=
  let make {kind : Set} (mcase : Manager_result.case kind)
    : Data_encoding.case packed_successful_manager_operation_result :=
    let 'Manager_result.MCase res_case := mcase in
    let 'existT _ __MCase_'a res_case :=
      existT (A := Set) (fun __MCase_'a ⇒ Manager_result.case.MCase __MCase_'a)
        _ res_case in
    let 'Alpha_context.Operation.Encoding.Manager_operations.MCase op_case :=
      res_case.(Manager_result.case.MCase.op_case) in
    Data_encoding.case_value
      op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name)
      None
      (Data_encoding.Tag
        op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.tag))
      (Data_encoding.merge_objs
        (Data_encoding.obj1
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name))))
        res_case.(Manager_result.case.MCase.encoding))
      (fun (res : packed_successful_manager_operation_result) ⇒
        match res_case.(Manager_result.case.MCase.select) res with
        | Some res ⇒ Some (tt, (res_case.(Manager_result.case.MCase.proj) res))
        | None ⇒ None
        end)
      (fun (function_parameter : unit × __MCase_'a) ⇒
        let '(_, res) := function_parameter in
        Successful_manager_result (res_case.(Manager_result.case.MCase.inj) res))
    in
  Data_encoding.def "operation.alpha.successful_manager_operation_result" None
    None
    (Data_encoding.union None
      [
        make Manager_result.reveal_case;
        make Manager_result.transaction_case;
        make Manager_result.origination_case;
        make Manager_result.delegation_case;
        make Manager_result.update_consensus_key_case;
        make Manager_result.set_deposits_limit_case;
        make Manager_result.increase_paid_storage_case;
        make Manager_result.sc_rollup_originate_case
      ]).

Records for the constructor parameters

Module ConstructorRecords_contents_result.
  Module contents_result.
    Module Preendorsement_result.
      Record record {balance_updates delegate consensus_key preendorsement_power
        : Set} : Set := Build {
        balance_updates : balance_updates;
        delegate : delegate;
        consensus_key : consensus_key;
        preendorsement_power : preendorsement_power;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
        balance_updates
        (r :
          record t_balance_updates t_delegate t_consensus_key
            t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_consensus_key
          t_preendorsement_power balance_updates r.(delegate) r.(consensus_key)
          r.(preendorsement_power).
      Definition with_delegate
        {t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
        delegate
        (r :
          record t_balance_updates t_delegate t_consensus_key
            t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_consensus_key
          t_preendorsement_power r.(balance_updates) delegate r.(consensus_key)
          r.(preendorsement_power).
      Definition with_consensus_key
        {t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
        consensus_key
        (r :
          record t_balance_updates t_delegate t_consensus_key
            t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_consensus_key
          t_preendorsement_power r.(balance_updates) r.(delegate) consensus_key
          r.(preendorsement_power).
      Definition with_preendorsement_power
        {t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
        preendorsement_power
        (r :
          record t_balance_updates t_delegate t_consensus_key
            t_preendorsement_power) :=
        Build t_balance_updates t_delegate t_consensus_key
          t_preendorsement_power r.(balance_updates) r.(delegate)
          r.(consensus_key) preendorsement_power.
    End Preendorsement_result.
    Definition Preendorsement_result_skeleton := Preendorsement_result.record.

    Module Endorsement_result.
      Record record {balance_updates delegate consensus_key endorsement_power :
        Set} : Set := Build {
        balance_updates : balance_updates;
        delegate : delegate;
        consensus_key : consensus_key;
        endorsement_power : endorsement_power;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_delegate t_consensus_key t_endorsement_power}
        balance_updates
        (r :
          record t_balance_updates t_delegate t_consensus_key
            t_endorsement_power) :=
        Build t_balance_updates t_delegate t_consensus_key t_endorsement_power
          balance_updates r.(delegate) r.(consensus_key) r.(endorsement_power).
      Definition with_delegate
        {t_balance_updates t_delegate t_consensus_key t_endorsement_power}
        delegate
        (r :
          record t_balance_updates