🏗️ 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 t_delegate t_consensus_key
            t_endorsement_power) :=
        Build t_balance_updates t_delegate t_consensus_key t_endorsement_power
          r.(balance_updates) delegate r.(consensus_key) r.(endorsement_power).
      Definition with_consensus_key
        {t_balance_updates t_delegate t_consensus_key t_endorsement_power}
        consensus_key
        (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
          r.(balance_updates) r.(delegate) consensus_key r.(endorsement_power).
      Definition with_endorsement_power
        {t_balance_updates t_delegate t_consensus_key t_endorsement_power}
        endorsement_power
        (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
          r.(balance_updates) r.(delegate) r.(consensus_key) endorsement_power.
    End Endorsement_result.
    Definition Endorsement_result_skeleton := Endorsement_result.record.

    Module Dal_attestation_result.
      Record record {delegate : Set} : Set := Build {
        delegate : delegate;
      }.
      Arguments record : clear implicits.
      Definition with_delegate {t_delegate} delegate (r : record t_delegate) :=
        Build t_delegate delegate.
    End Dal_attestation_result.
    Definition Dal_attestation_result_skeleton := Dal_attestation_result.record.

    Module Drain_delegate_result.
      Record record {balance_updates allocated_destination_contract : Set} : Set := Build {
        balance_updates : balance_updates;
        allocated_destination_contract : allocated_destination_contract;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_allocated_destination_contract} balance_updates
        (r : record t_balance_updates t_allocated_destination_contract) :=
        Build t_balance_updates t_allocated_destination_contract balance_updates
          r.(allocated_destination_contract).
      Definition with_allocated_destination_contract
        {t_balance_updates t_allocated_destination_contract}
        allocated_destination_contract
        (r : record t_balance_updates t_allocated_destination_contract) :=
        Build t_balance_updates t_allocated_destination_contract
          r.(balance_updates) allocated_destination_contract.
    End Drain_delegate_result.
    Definition Drain_delegate_result_skeleton := Drain_delegate_result.record.

    Module Manager_operation_result.
      Record record {balance_updates operation_result internal_operation_results
        : Set} : Set := Build {
        balance_updates : balance_updates;
        operation_result : operation_result;
        internal_operation_results : internal_operation_results;
      }.
      Arguments record : clear implicits.
      Definition with_balance_updates
        {t_balance_updates t_operation_result t_internal_operation_results}
        balance_updates
        (r :
          record t_balance_updates t_operation_result
            t_internal_operation_results) :=
        Build t_balance_updates t_operation_result t_internal_operation_results
          balance_updates r.(operation_result) r.(internal_operation_results).
      Definition with_operation_result
        {t_balance_updates t_operation_result t_internal_operation_results}
        operation_result
        (r :
          record t_balance_updates t_operation_result
            t_internal_operation_results) :=
        Build t_balance_updates t_operation_result t_internal_operation_results
          r.(balance_updates) operation_result r.(internal_operation_results).
      Definition with_internal_operation_results
        {t_balance_updates t_operation_result t_internal_operation_results}
        internal_operation_results
        (r :
          record t_balance_updates t_operation_result
            t_internal_operation_results) :=
        Build t_balance_updates t_operation_result t_internal_operation_results
          r.(balance_updates) r.(operation_result) internal_operation_results.
    End Manager_operation_result.
    Definition Manager_operation_result_skeleton :=
      Manager_operation_result.record.
  End contents_result.
End ConstructorRecords_contents_result.
Import ConstructorRecords_contents_result.

Reserved Notation "'contents_result.Preendorsement_result".
Reserved Notation "'contents_result.Endorsement_result".
Reserved Notation "'contents_result.Dal_attestation_result".
Reserved Notation "'contents_result.Drain_delegate_result".
Reserved Notation "'contents_result.Manager_operation_result".

Inductive contents_result : Set :=
| Preendorsement_result :
  'contents_result.Preendorsement_result → contents_result
| Endorsement_result : 'contents_result.Endorsement_result → contents_result
| Dal_attestation_result :
  'contents_result.Dal_attestation_result → contents_result
| Seed_nonce_revelation_result :
  Alpha_context.Receipt.balance_updates → contents_result
| Vdf_revelation_result :
  Alpha_context.Receipt.balance_updates → contents_result
| Double_endorsement_evidence_result :
  Alpha_context.Receipt.balance_updates → contents_result
| Double_preendorsement_evidence_result :
  Alpha_context.Receipt.balance_updates → contents_result
| Double_baking_evidence_result :
  Alpha_context.Receipt.balance_updates → contents_result
| Activate_account_result :
  Alpha_context.Receipt.balance_updates → contents_result
| Proposals_result : contents_result
| Ballot_result : contents_result
| Drain_delegate_result :
  'contents_result.Drain_delegate_result → contents_result
| Manager_operation_result :
  'contents_result.Manager_operation_result → contents_result

where "'contents_result.Preendorsement_result" :=
  (contents_result.Preendorsement_result_skeleton
    Alpha_context.Receipt.balance_updates Signature.public_key_hash
    Signature.public_key_hash int)
and "'contents_result.Endorsement_result" :=
  (contents_result.Endorsement_result_skeleton
    Alpha_context.Receipt.balance_updates Signature.public_key_hash
    Signature.public_key_hash int)
and "'contents_result.Dal_attestation_result" :=
  (contents_result.Dal_attestation_result_skeleton Signature.public_key_hash)
and "'contents_result.Drain_delegate_result" :=
  (contents_result.Drain_delegate_result_skeleton
    Alpha_context.Receipt.balance_updates bool)
and "'contents_result.Manager_operation_result" :=
  (contents_result.Manager_operation_result_skeleton
    Alpha_context.Receipt.balance_updates manager_operation_result
    (list Apply_internal_results.packed_internal_operation_result)).

Module contents_result.
  Include ConstructorRecords_contents_result.contents_result.
  Definition Preendorsement_result := 'contents_result.Preendorsement_result.
  Definition Endorsement_result := 'contents_result.Endorsement_result.
  Definition Dal_attestation_result := 'contents_result.Dal_attestation_result.
  Definition Drain_delegate_result := 'contents_result.Drain_delegate_result.
  Definition Manager_operation_result :=
    'contents_result.Manager_operation_result.
End contents_result.

Inductive packed_contents_result : Set :=
| Contents_result : contents_result → packed_contents_result.

Inductive packed_contents_and_result : Set :=
| Contents_and_result :
  Alpha_context.Operation.contents → contents_result →
  packed_contents_and_result.

Inductive eq : Set :=
| Eq : eq.

Definition equal_manager_kind
  (ka : Alpha_context.Kind.manager) (kb : Alpha_context.Kind.manager)
  : option eq :=
  match (ka, kb) with
  |
    (Alpha_context.Kind.Reveal_manager_kind,
      Alpha_context.Kind.Reveal_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Reveal_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Transaction_manager_kind,
      Alpha_context.Kind.Transaction_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Transaction_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Origination_manager_kind,
      Alpha_context.Kind.Origination_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Origination_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Delegation_manager_kind,
      Alpha_context.Kind.Delegation_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Delegation_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Update_consensus_key_manager_kind,
      Alpha_context.Kind.Update_consensus_key_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Update_consensus_key_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Register_global_constant_manager_kind,
      Alpha_context.Kind.Register_global_constant_manager_kind) ⇒ Some Eq
  |
    (Alpha_context.Kind.Event_manager_kind,
      Alpha_context.Kind.Event_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Event_manager_kind, _) ⇒ None
  | (Alpha_context.Kind.Register_global_constant_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Set_deposits_limit_manager_kind,
      Alpha_context.Kind.Set_deposits_limit_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Set_deposits_limit_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Increase_paid_storage_manager_kind,
      Alpha_context.Kind.Increase_paid_storage_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Increase_paid_storage_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_origination_manager_kind,
      Alpha_context.Kind.Tx_rollup_origination_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_origination_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind,
      Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_commit_manager_kind,
      Alpha_context.Kind.Tx_rollup_commit_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_commit_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_return_bond_manager_kind,
      Alpha_context.Kind.Tx_rollup_return_bond_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_return_bond_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind,
      Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind,
      Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_rejection_manager_kind,
      Alpha_context.Kind.Tx_rollup_rejection_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_rejection_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind,
      Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Transfer_ticket_manager_kind,
      Alpha_context.Kind.Transfer_ticket_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Transfer_ticket_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Dal_publish_slot_header_manager_kind,
      Alpha_context.Kind.Dal_publish_slot_header_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Dal_publish_slot_header_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_originate_manager_kind,
      Alpha_context.Kind.Sc_rollup_originate_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_originate_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_add_messages_manager_kind,
      Alpha_context.Kind.Sc_rollup_add_messages_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_add_messages_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_cement_manager_kind,
      Alpha_context.Kind.Sc_rollup_cement_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_cement_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_publish_manager_kind,
      Alpha_context.Kind.Sc_rollup_publish_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_publish_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_refute_manager_kind,
      Alpha_context.Kind.Sc_rollup_refute_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_refute_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_timeout_manager_kind,
      Alpha_context.Kind.Sc_rollup_timeout_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_timeout_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind,
      Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind) ⇒
    Some Eq
  | (Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind, _) ⇒
    None
  |
    (Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind,
      Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Zk_rollup_origination_manager_kind,
      Alpha_context.Kind.Zk_rollup_origination_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Zk_rollup_origination_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Zk_rollup_publish_manager_kind,
      Alpha_context.Kind.Zk_rollup_publish_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Zk_rollup_publish_manager_kind, _) ⇒ None
  |
    (Alpha_context.Kind.Zk_rollup_update_manager_kind,
      Alpha_context.Kind.Zk_rollup_update_manager_kind) ⇒ Some Eq
  | (Alpha_context.Kind.Zk_rollup_update_manager_kind, _) ⇒ None
  end.

Module Encoding.

Records for the constructor parameters

  Module ConstructorRecords_case.
    Module case.
      Module Case.
        Record record {op_case encoding select mselect proj inj : Set} : Set := Build {
          op_case : op_case;
          encoding : encoding;
          select : select;
          mselect : mselect;
          proj : proj;
          inj : inj;
        }.
        Arguments record : clear implicits.
        Definition with_op_case
          {t_op_case t_encoding t_select t_mselect t_proj t_inj} op_case
          (r : record t_op_case t_encoding t_select t_mselect t_proj t_inj) :=
          Build t_op_case t_encoding t_select t_mselect t_proj t_inj op_case
            r.(encoding) r.(select) r.(mselect) r.(proj) r.(inj).
        Definition with_encoding
          {t_op_case t_encoding t_select t_mselect t_proj t_inj} encoding
          (r : record t_op_case t_encoding t_select t_mselect t_proj t_inj) :=
          Build t_op_case t_encoding t_select t_mselect t_proj t_inj r.(op_case)
            encoding r.(select) r.(mselect) r.(proj) r.(inj).
        Definition with_select
          {t_op_case t_encoding t_select t_mselect t_proj t_inj} select
          (r : record t_op_case t_encoding t_select t_mselect t_proj t_inj) :=
          Build t_op_case t_encoding t_select t_mselect t_proj t_inj r.(op_case)
            r.(encoding) select r.(mselect) r.(proj) r.(inj).
        Definition with_mselect
          {t_op_case t_encoding t_select t_mselect t_proj t_inj} mselect
          (r : record t_op_case t_encoding t_select t_mselect t_proj t_inj) :=
          Build t_op_case t_encoding t_select t_mselect t_proj t_inj r.(op_case)
            r.(encoding) r.(select) mselect r.(proj) r.(inj).
        Definition with_proj
          {t_op_case t_encoding t_select t_mselect t_proj t_inj} proj
          (r : record t_op_case t_encoding t_select t_mselect t_proj t_inj) :=
          Build t_op_case t_encoding t_select t_mselect t_proj t_inj r.(op_case)
            r.(encoding) r.(select) r.(mselect) proj r.(inj).
        Definition with_inj
          {t_op_case t_encoding t_select t_mselect t_proj t_inj} inj
          (r : record t_op_case t_encoding t_select t_mselect t_proj t_inj) :=
          Build t_op_case t_encoding t_select t_mselect t_proj t_inj r.(op_case)
            r.(encoding) r.(select) r.(mselect) r.(proj) inj.
      End Case.
      Definition Case_skeleton := Case.record.
    End case.
  End ConstructorRecords_case.
  Import ConstructorRecords_case.

  Reserved Notation "'case.Case".

  Inductive case (kind : Set) : Set :=
  | Case : ∀ {a : Set}, 'case.Case kind a → case kind
  
  where "'case.Case" :=
    (fun (t_kind t_a : Set) ⇒ case.Case_skeleton
      (Alpha_context.Operation.Encoding.case t_kind) (Data_encoding.t t_a)
      (packed_contents_result → option contents_result)
      (packed_contents_and_result →
      option (Alpha_context.contents × contents_result))
      (contents_result → t_a) (t_a → contents_result)).

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

  Arguments Case {_ _}.

  Definition tagged_case {A B : Set}
    (tag : Data_encoding.case_tag) (name : string)
    (args : Data_encoding.encoding A) (proj : B → option A) (inj : A → B)
    : Data_encoding.case B :=
    Data_encoding.case_value (String.capitalize_ascii name) None tag
      (Data_encoding.merge_objs
        (Data_encoding.obj1
          (Data_encoding.req None None "kind" (Data_encoding.constant name)))
        args)
      (fun (x_value : B) ⇒
        match proj x_value with
        | None ⇒ None
        | Some x_value ⇒ Some (tt, x_value)
        end)
      (fun (function_parameter : unit × A) ⇒
        let '(_, x_value) := function_parameter in
        inj x_value).

  Definition preendorsement_case : case Alpha_context.Kind.preendorsement :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.preendorsement_case;
        case.Case.encoding :=
          Data_encoding.obj4
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.req None None "delegate"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "preendorsement_power"
              Data_encoding.int31)
            (Data_encoding.req None None "consensus_key"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Preendorsement_result _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Preendorsement _) as op) res
              ⇒ Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            |
              Preendorsement_result {|
                contents_result.Preendorsement_result.balance_updates := balance_updates;
                  contents_result.Preendorsement_result.delegate := delegate;
                  contents_result.Preendorsement_result.consensus_key :=
                    consensus_key;
                  contents_result.Preendorsement_result.preendorsement_power :=
                    preendorsement_power
                  |} ⇒
              (balance_updates, delegate, preendorsement_power, consensus_key)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Alpha_context.Receipt.balance_updates × Signature.public_key_hash ×
              int × Signature.public_key_hash) ⇒
            let
              '(balance_updates, delegate, preendorsement_power, consensus_key) :=
              function_parameter in
            Preendorsement_result
              {|
                contents_result.Preendorsement_result.balance_updates :=
                  balance_updates;
                contents_result.Preendorsement_result.delegate := delegate;
                contents_result.Preendorsement_result.consensus_key :=
                  consensus_key;
                contents_result.Preendorsement_result.preendorsement_power :=
                  preendorsement_power; |}; |}.

  Definition endorsement_case : case Alpha_context.Kind.endorsement :=
    Case
      {| case.Case.op_case := Alpha_context.Operation.Encoding.endorsement_case;
        case.Case.encoding :=
          Data_encoding.obj4
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.req None None "delegate"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "endorsement_power" Data_encoding.int31)
            (Data_encoding.req None None "consensus_key"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Endorsement_result _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Endorsement _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            |
              Endorsement_result {|
                contents_result.Endorsement_result.balance_updates := balance_updates;
                  contents_result.Endorsement_result.delegate := delegate;
                  contents_result.Endorsement_result.consensus_key :=
                    consensus_key;
                  contents_result.Endorsement_result.endorsement_power :=
                    endorsement_power
                  |} ⇒
              (balance_updates, delegate, endorsement_power, consensus_key)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Alpha_context.Receipt.balance_updates × Signature.public_key_hash ×
              int × Signature.public_key_hash) ⇒
            let
              '(balance_updates, delegate, endorsement_power, consensus_key) :=
              function_parameter in
            Endorsement_result
              {|
                contents_result.Endorsement_result.balance_updates :=
                  balance_updates;
                contents_result.Endorsement_result.delegate := delegate;
                contents_result.Endorsement_result.consensus_key :=
                  consensus_key;
                contents_result.Endorsement_result.endorsement_power :=
                  endorsement_power; |}; |}.

  Definition dal_attestation_case : case Alpha_context.Kind.dal_attestation :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.dal_attestation_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.req None None "delegate"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Dal_attestation_result _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Dal_attestation _) as op) res
              ⇒ Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            |
              Dal_attestation_result {|
                contents_result.Dal_attestation_result.delegate := delegate
                  |} ⇒ delegate
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (delegate : Signature.public_key_hash) ⇒
            Dal_attestation_result
              {| contents_result.Dal_attestation_result.delegate := delegate; |};
        |}.

  Definition seed_nonce_revelation_case
    : case Alpha_context.Kind.seed_nonce_revelation :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.seed_nonce_revelation_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Seed_nonce_revelation_result _) as op) ⇒
              Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            |
              Contents_and_result
                ((Alpha_context.Seed_nonce_revelation _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Seed_nonce_revelation_result bus ⇒ bus
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (bus : Alpha_context.Receipt.balance_updates) ⇒
            Seed_nonce_revelation_result bus; |}.

  Definition vdf_revelation_case : case Alpha_context.Kind.vdf_revelation :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.vdf_revelation_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Vdf_revelation_result _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Vdf_revelation _) as op) res
              ⇒ Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Vdf_revelation_result bus ⇒ bus
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (bus : Alpha_context.Receipt.balance_updates) ⇒
            Vdf_revelation_result bus; |}.

  Definition double_endorsement_evidence_case
    : case Alpha_context.Kind.double_endorsement_evidence :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.double_endorsement_evidence_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Double_endorsement_evidence_result _) as op) ⇒
              Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            |
              Contents_and_result
                ((Alpha_context.Double_endorsement_evidence _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Double_endorsement_evidence_result bus ⇒ bus
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (bus : Alpha_context.Receipt.balance_updates) ⇒
            Double_endorsement_evidence_result bus; |}.

  Definition double_preendorsement_evidence_case
    : case Alpha_context.Kind.double_preendorsement_evidence :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.double_preendorsement_evidence_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Double_preendorsement_evidence_result _) as op)
              ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            |
              Contents_and_result
                ((Alpha_context.Double_preendorsement_evidence _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Double_preendorsement_evidence_result bus ⇒ bus
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (bus : Alpha_context.Receipt.balance_updates) ⇒
            Double_preendorsement_evidence_result bus; |}.

  Definition double_baking_evidence_case
    : case Alpha_context.Kind.double_baking_evidence :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.double_baking_evidence_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Double_baking_evidence_result _) as op) ⇒
              Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            |
              Contents_and_result
                ((Alpha_context.Double_baking_evidence _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Double_baking_evidence_result bus ⇒ bus
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (bus : Alpha_context.Receipt.balance_updates) ⇒
            Double_baking_evidence_result bus; |}.

  Definition activate_account_case : case Alpha_context.Kind.activate_account :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.activate_account_case;
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Activate_account_result _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Activate_account _) as op) res
              ⇒ Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Activate_account_result bus ⇒ bus
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (bus : Alpha_context.Receipt.balance_updates) ⇒
            Activate_account_result bus; |}.

  Definition proposals_case : case Alpha_context.Kind.proposals :=
    Case
      {| case.Case.op_case := Alpha_context.Operation.Encoding.proposals_case;
        case.Case.encoding := Data_encoding.empty;
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result (Proposals_result as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Proposals _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Proposals_result ⇒ tt
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Proposals_result; |}.

  Definition ballot_case : case Alpha_context.Kind.ballot :=
    Case
      {| case.Case.op_case := Alpha_context.Operation.Encoding.ballot_case;
        case.Case.encoding := Data_encoding.empty;
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result (Ballot_result as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Ballot _) as op) res ⇒
              Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            | Ballot_result ⇒ tt
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Ballot_result; |}.

  Definition drain_delegate_case : case Alpha_context.Kind.drain_delegate :=
    Case
      {|
        case.Case.op_case :=
          Alpha_context.Operation.Encoding.drain_delegate_case;
        case.Case.encoding :=
          Data_encoding.obj2
            (Data_encoding.dft None None "balance_updates"
              Alpha_context.Receipt.balance_updates_encoding nil)
            (Data_encoding.dft None None "allocated_destination_contract"
              Data_encoding.bool_value false);
        case.Case.select :=
          fun (function_parameter : packed_contents_result) ⇒
            match function_parameter with
            | Contents_result ((Drain_delegate_result _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.mselect :=
          fun (function_parameter : packed_contents_and_result) ⇒
            match function_parameter with
            | Contents_and_result ((Alpha_context.Drain_delegate _) as op) res
              ⇒ Some (op, res)
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents_result) ⇒
            match function_parameter with
            |
              Drain_delegate_result {|
                contents_result.Drain_delegate_result.balance_updates := balance_updates;
                  contents_result.Drain_delegate_result.allocated_destination_contract
                    := allocated_destination_contract
                  |} ⇒ (balance_updates, allocated_destination_contract)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Alpha_context.Receipt.balance_updates × bool) ⇒
            let '(balance_updates, allocated_destination_contract) :=
              function_parameter in
            Drain_delegate_result
              {|
                contents_result.Drain_delegate_result.balance_updates :=
                  balance_updates;
                contents_result.Drain_delegate_result.allocated_destination_contract
                  := allocated_destination_contract; |}; |}.

  Definition make_manager_case {kind : Set}
    (function_parameter :
      Alpha_context.Operation.Encoding.case Alpha_context.Kind.manager)
    : Manager_result.case kind →
    (packed_contents_and_result →
    option (Alpha_context.contents × contents_result)) →
    case Alpha_context.Kind.manager :=
    let 'Alpha_context.Operation.Encoding.Case op_case := function_parameter in
    fun (function_parameter : Manager_result.case kind) ⇒
      let 'Manager_result.MCase res_case := function_parameter in
      fun (mselect :
        packed_contents_and_result →
        option (Alpha_context.contents × contents_result)) ⇒
        Case
          {| case.Case.op_case := Alpha_context.Operation.Encoding.Case op_case;
            case.Case.encoding :=
              Data_encoding.obj3
                (Data_encoding.dft None None "balance_updates"
                  Alpha_context.Receipt.balance_updates_encoding nil)
                (Data_encoding.req None None "operation_result"
                  res_case.(Manager_result.case.MCase.t))
                (Data_encoding.dft None None "internal_operation_results"
                  (Data_encoding.list_value None
                    Apply_internal_results.internal_operation_result_encoding)
                  nil);
            case.Case.select :=
              fun (function_parameter : packed_contents_result) ⇒
                match function_parameter with
                |
                  Contents_result
                    (Manager_operation_result
                      ({|
                        contents_result.Manager_operation_result.operation_result :=
                          Apply_operation_result.Applied res
                          |} as op)) ⇒
                  let '[op, res] :=
                    cast
                      [contents_result.Manager_operation_result **
                        successful_manager_operation_result] [op, res] in
                  match
                    res_case.(Manager_result.case.MCase.select)
                      (Successful_manager_result res) with
                  | Some res ⇒
                    Some
                      (Manager_operation_result
                        (contents_result.Manager_operation_result.with_operation_result
                          (Apply_operation_result.Applied res) op))
                  | None ⇒ None
                  end
                |
                  Contents_result
                    (Manager_operation_result
                      ({|
                        contents_result.Manager_operation_result.operation_result :=
                          Apply_operation_result.Backtracked res errs
                          |} as op)) ⇒
                  let '[op, errs, res] :=
                    cast
                      [contents_result.Manager_operation_result **
                        option (Error_monad.trace Error_monad._error) **
                        successful_manager_operation_result] [op, errs, res] in
                  match
                    res_case.(Manager_result.case.MCase.select)
                      (Successful_manager_result res) with
                  | Some res ⇒
                    Some
                      (Manager_operation_result
                        (contents_result.Manager_operation_result.with_operation_result
                          (Apply_operation_result.Backtracked res errs) op))
                  | None ⇒ None
                  end
                |
                  Contents_result
                    (Manager_operation_result
                      ({|
                        contents_result.Manager_operation_result.operation_result :=
                          Apply_operation_result.Skipped kind_value
                          |} as op)) ⇒
                  let '[op, kind_value] :=
                    cast
                      [contents_result.Manager_operation_result **
                        Alpha_context.Kind.manager] [op, kind_value] in
                  match
                    equal_manager_kind kind_value
                      res_case.(Manager_result.case.MCase.kind) with
                  | None ⇒ None
                  | Some Eq ⇒
                    Some
                      (Manager_operation_result
                        (contents_result.Manager_operation_result.with_operation_result
                          (Apply_operation_result.Skipped kind_value) op))
                  end
                |
                  Contents_result
                    (Manager_operation_result
                      ({|
                        contents_result.Manager_operation_result.operation_result :=
                          Apply_operation_result.Failed kind_value errs
                          |} as op)) ⇒
                  let '[op, errs, kind_value] :=
                    cast
                      [contents_result.Manager_operation_result **
                        Error_monad.trace Error_monad._error **
                        Alpha_context.Kind.manager] [op, errs, kind_value] in
                  match
                    equal_manager_kind kind_value
                      res_case.(Manager_result.case.MCase.kind) with
                  | None ⇒ None
                  | Some Eq ⇒
                    Some
                      (Manager_operation_result
                        (contents_result.Manager_operation_result.with_operation_result
                          (Apply_operation_result.Failed kind_value errs) op))
                  end
                | Contents_result (Preendorsement_result _) ⇒ None
                | Contents_result (Endorsement_result _) ⇒ None
                | Contents_result (Dal_attestation_result _) ⇒ None
                | Contents_result Ballot_result ⇒ None
                | Contents_result (Seed_nonce_revelation_result _) ⇒ None
                | Contents_result (Vdf_revelation_result _) ⇒ None
                | Contents_result (Double_endorsement_evidence_result _) ⇒ None
                | Contents_result (Double_preendorsement_evidence_result _) ⇒
                  None
                | Contents_result (Double_baking_evidence_result _) ⇒ None
                | Contents_result (Activate_account_result _) ⇒ None
                | Contents_result (Drain_delegate_result _) ⇒ None
                | Contents_result Proposals_result ⇒ None
                end; case.Case.mselect := mselect;
            case.Case.proj :=
              fun (function_parameter : contents_result) ⇒
                match function_parameter with
                |
                  Manager_operation_result {|
                    contents_result.Manager_operation_result.balance_updates := bus;
                      contents_result.Manager_operation_result.operation_result
                        := r_value;
                      contents_result.Manager_operation_result.internal_operation_results
                        := rs
                      |} ⇒ (bus, r_value, rs)
                | _ ⇒ unreachable_gadt_branch
                end;
            case.Case.inj :=
              fun (function_parameter :
                Alpha_context.Receipt.balance_updates × manager_operation_result
                  × list Apply_internal_results.packed_internal_operation_result)
                ⇒
                let '(bus, r_value, rs) := function_parameter in
                Manager_operation_result
                  {|
                    contents_result.Manager_operation_result.balance_updates :=
                      bus;
                    contents_result.Manager_operation_result.operation_result :=
                      r_value;
                    contents_result.Manager_operation_result.internal_operation_results
                      := rs; |}; |}.

  Definition reveal_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.reveal_case
      Manager_result.reveal_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation := Alpha_context.Reveal _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition transaction_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.transaction_case
      Manager_result.transaction_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Transaction _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition origination_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.origination_case
      Manager_result.origination_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Origination _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition delegation_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.delegation_case
      Manager_result.delegation_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Delegation _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition update_consensus_key_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.update_consensus_key_case
      Manager_result.update_consensus_key_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Update_consensus_key _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition register_global_constant_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.register_global_constant_case
      Manager_result.register_global_constant_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Register_global_constant _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition set_deposits_limit_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.set_deposits_limit_case
      Manager_result.set_deposits_limit_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Set_deposits_limit _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition increase_paid_storage_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.increase_paid_storage_case
      Manager_result.increase_paid_storage_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Increase_paid_storage _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_origination_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.tx_rollup_origination_case
      Manager_result.tx_rollup_origination_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_origination
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_submit_batch_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.tx_rollup_submit_batch_case
      Manager_result.tx_rollup_submit_batch_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_submit_batch _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_commit_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.tx_rollup_commit_case
      Manager_result.tx_rollup_commit_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_commit _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_return_bond_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.tx_rollup_return_bond_case
      Manager_result.tx_rollup_return_bond_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_return_bond _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_finalize_commitment_case
    : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.tx_rollup_finalize_commitment_case
      Manager_result.tx_rollup_finalize_commitment_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_finalize_commitment _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_remove_commitment_case
    : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.tx_rollup_remove_commitment_case
      Manager_result.tx_rollup_remove_commitment_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_remove_commitment _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_rejection_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.tx_rollup_rejection_case
      Manager_result.tx_rollup_rejection_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_rejection _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition tx_rollup_dispatch_tickets_case
    : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.tx_rollup_dispatch_tickets_case
      Manager_result.tx_rollup_dispatch_tickets_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Tx_rollup_dispatch_tickets _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition transfer_ticket_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.transfer_ticket_case
      Manager_result.transfer_ticket_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Transfer_ticket _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition dal_publish_slot_header_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.dal_publish_slot_header_case
      Manager_result.dal_publish_slot_header_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Dal_publish_slot_header _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_originate_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.sc_rollup_originate_case
      Manager_result.sc_rollup_originate_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_originate _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_add_messages_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.sc_rollup_add_messages_case
      Manager_result.sc_rollup_add_messages_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_add_messages _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_cement_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.sc_rollup_cement_case
      Manager_result.sc_rollup_cement_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_cement _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_publish_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.sc_rollup_publish_case
      Manager_result.sc_rollup_publish_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_publish _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_refute_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.sc_rollup_refute_case
      Manager_result.sc_rollup_refute_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_refute _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_timeout_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.sc_rollup_timeout_case
      Manager_result.sc_rollup_timeout_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_timeout _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_execute_outbox_message_case
    : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.sc_rollup_execute_outbox_message_case
      Manager_result.sc_rollup_execute_outbox_message_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_execute_outbox_message _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition sc_rollup_recover_bond_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.sc_rollup_recover_bond_case
      Manager_result.sc_rollup_recover_bond_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Sc_rollup_recover_bond _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition zk_rollup_origination_case : case Alpha_context.Kind.manager :=
    make_manager_case
      Alpha_context.Operation.Encoding.zk_rollup_origination_case
      Manager_result.zk_rollup_origination_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Zk_rollup_origination _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition zk_rollup_publish_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.zk_rollup_publish_case
      Manager_result.zk_rollup_publish_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Zk_rollup_publish _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).

  Definition zk_rollup_update_case : case Alpha_context.Kind.manager :=
    make_manager_case Alpha_context.Operation.Encoding.zk_rollup_update_case
      Manager_result.zk_rollup_update_case
      (fun (function_parameter : packed_contents_and_result) ⇒
        match function_parameter with
        |
          Contents_and_result
            ((Alpha_context.Manager_operation {|
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Zk_rollup_update _
                |}) as op) res ⇒ Some (op, res)
        | _ ⇒ None
        end).
End Encoding.

Definition contents_result_encoding
  : Data_encoding.encoding packed_contents_result :=
  let make {A : Set} (case_description : Encoding.case A)
    : Data_encoding.case packed_contents_result :=
    let
      'Encoding.Case {|
        Encoding.case.Case.op_case :=
          Alpha_context.Operation.Encoding.Case {|
            Alpha_context.Operation.Encoding.case.Case.tag := tag;
              Alpha_context.Operation.Encoding.case.Case.name :=
                name
              |};
          Encoding.case.Case.encoding := encoding;
          Encoding.case.Case.select := select;
          Encoding.case.Case.mselect := _;
          Encoding.case.Case.proj := proj;
          Encoding.case.Case.inj := inj
          |} := case_description in
    let 'existT _ __Case_'a [inj, proj, select, encoding, name, tag] :=
      existT (A := Set)
        (fun __Case_'a ⇒
          [__Case_'a → contents_result ** contents_result → __Case_'a **
            packed_contents_result → option contents_result **
            Data_encoding.t __Case_'a ** string ** int]) _
        [inj, proj, select, encoding, name, tag] in
    let proj (x_value : packed_contents_result) : option __Case_'a :=
      match select x_value with
      | None ⇒ None
      | Some x_value ⇒ Some (proj x_value)
      end in
    let inj (x_value : __Case_'a) : packed_contents_result :=
      Contents_result (inj x_value) in
    Encoding.tagged_case (Data_encoding.Tag tag) name encoding proj inj in
  Data_encoding.def "operation.alpha.contents_result" None None
    (Data_encoding.union None
      [
        make Encoding.seed_nonce_revelation_case;
        make Encoding.vdf_revelation_case;
        make Encoding.endorsement_case;
        make Encoding.preendorsement_case;
        make Encoding.dal_attestation_case;
        make Encoding.double_preendorsement_evidence_case;
        make Encoding.double_endorsement_evidence_case;
        make Encoding.double_baking_evidence_case;
        make Encoding.activate_account_case;
        make Encoding.proposals_case;
        make Encoding.ballot_case;
        make Encoding.drain_delegate_case;
        make Encoding.reveal_case;
        make Encoding.transaction_case;
        make Encoding.origination_case;
        make Encoding.delegation_case;
        make Encoding.register_global_constant_case;
        make Encoding.set_deposits_limit_case;
        make Encoding.increase_paid_storage_case;
        make Encoding.update_consensus_key_case;
        make Encoding.tx_rollup_origination_case;
        make Encoding.tx_rollup_submit_batch_case;
        make Encoding.tx_rollup_commit_case;
        make Encoding.tx_rollup_return_bond_case;
        make Encoding.tx_rollup_finalize_commitment_case;
        make Encoding.tx_rollup_remove_commitment_case;
        make Encoding.tx_rollup_rejection_case;
        make Encoding.tx_rollup_dispatch_tickets_case;
        make Encoding.transfer_ticket_case;
        make Encoding.dal_publish_slot_header_case;
        make Encoding.sc_rollup_originate_case;
        make Encoding.sc_rollup_add_messages_case;
        make Encoding.sc_rollup_cement_case;
        make Encoding.sc_rollup_publish_case;
        make Encoding.sc_rollup_refute_case;
        make Encoding.sc_rollup_timeout_case;
        make Encoding.sc_rollup_execute_outbox_message_case;
        make Encoding.sc_rollup_recover_bond_case;
        make Encoding.zk_rollup_origination_case;
        make Encoding.zk_rollup_publish_case;
        make Encoding.zk_rollup_update_case
      ]).

Definition contents_and_result_encoding
  : Data_encoding.encoding packed_contents_and_result :=
  let make {A : Set} (case_description : Encoding.case A)
    : Data_encoding.case packed_contents_and_result :=
    let
      'Encoding.Case {|
        Encoding.case.Case.op_case :=
          Alpha_context.Operation.Encoding.Case {|
            Alpha_context.Operation.Encoding.case.Case.tag := tag;
              Alpha_context.Operation.Encoding.case.Case.name :=
                name;
              Alpha_context.Operation.Encoding.case.Case.encoding :=
                encoding;
              Alpha_context.Operation.Encoding.case.Case.proj :=
                proj;
              Alpha_context.Operation.Encoding.case.Case.inj := inj
              |};
          Encoding.case.Case.encoding := meta_encoding;
          Encoding.case.Case.mselect := mselect;
          Encoding.case.Case.proj := meta_proj;
          Encoding.case.Case.inj := meta_inj
          |} := case_description in
    let 'existT _ [__Case_'a, __Case_'a1]
      [meta_inj, meta_proj, mselect, meta_encoding, inj, proj, encoding, name,
        tag] :=
      existT (A := [Set ** Set])
        (fun '[__Case_'a, __Case_'a1] ⇒
          [__Case_'a → contents_result ** contents_result → __Case_'a **
            packed_contents_and_result →
            option (Alpha_context.contents × contents_result) **
            Data_encoding.t __Case_'a **
            __Case_'a1 → Alpha_context.Operation.contents **
            Alpha_context.Operation.contents → __Case_'a1 **
            Data_encoding.t __Case_'a1 ** string ** int]) [_, _]
        [meta_inj, meta_proj, mselect, meta_encoding, inj, proj, encoding, name,
          tag] in
    let proj (c_value : packed_contents_and_result)
      : option (__Case_'a1 × __Case_'a) :=
      match mselect c_value with
      | Some (op, res) ⇒ Some ((proj op), (meta_proj res))
      | _ ⇒ None
      end in
    let inj (function_parameter : __Case_'a1 × __Case_'a)
      : packed_contents_and_result :=
      let '(op, res) := function_parameter in
      Contents_and_result (inj op) (meta_inj res) in
    let encoding :=
      Data_encoding.merge_objs encoding
        (Data_encoding.obj1
          (Data_encoding.req None None "metadata" meta_encoding)) in
    Encoding.tagged_case (Data_encoding.Tag tag) name encoding proj inj in
  Data_encoding.def "operation.alpha.operation_contents_and_result" None None
    (Data_encoding.union None
      [
        make Encoding.seed_nonce_revelation_case;
        make Encoding.vdf_revelation_case;
        make Encoding.endorsement_case;
        make Encoding.preendorsement_case;
        make Encoding.dal_attestation_case;
        make Encoding.double_preendorsement_evidence_case;
        make Encoding.double_endorsement_evidence_case;
        make Encoding.double_baking_evidence_case;
        make Encoding.activate_account_case;
        make Encoding.proposals_case;
        make Encoding.ballot_case;
        make Encoding.reveal_case;
        make Encoding.transaction_case;
        make Encoding.origination_case;
        make Encoding.delegation_case;
        make Encoding.register_global_constant_case;
        make Encoding.set_deposits_limit_case;
        make Encoding.increase_paid_storage_case;
        make Encoding.update_consensus_key_case;
        make Encoding.drain_delegate_case;
        make Encoding.tx_rollup_origination_case;
        make Encoding.tx_rollup_submit_batch_case;
        make Encoding.tx_rollup_commit_case;
        make Encoding.tx_rollup_return_bond_case;
        make Encoding.tx_rollup_finalize_commitment_case;
        make Encoding.tx_rollup_remove_commitment_case;
        make Encoding.tx_rollup_rejection_case;
        make Encoding.transfer_ticket_case;
        make Encoding.dal_publish_slot_header_case;
        make Encoding.tx_rollup_dispatch_tickets_case;
        make Encoding.sc_rollup_originate_case;
        make Encoding.sc_rollup_add_messages_case;
        make Encoding.sc_rollup_cement_case;
        make Encoding.sc_rollup_publish_case;
        make Encoding.sc_rollup_refute_case;
        make Encoding.sc_rollup_timeout_case;
        make Encoding.sc_rollup_execute_outbox_message_case;
        make Encoding.sc_rollup_recover_bond_case;
        make Encoding.zk_rollup_origination_case;
        make Encoding.zk_rollup_publish_case;
        make Encoding.zk_rollup_update_case
      ]).

Inductive contents_result_list : Set :=
| Single_result : contents_result → contents_result_list
| Cons_result : contents_result → contents_result_list → contents_result_list.

Inductive packed_contents_result_list : Set :=
| Contents_result_list : contents_result_list → packed_contents_result_list.

Fixpoint contents_result_list_to_list
  (function_parameter : contents_result_list) : list packed_contents_result :=
  match function_parameter with
  | Single_result o_value ⇒ [ Contents_result o_value ]
  | Cons_result o_value os ⇒
    cons (Contents_result o_value) (contents_result_list_to_list os)
  end.

Definition packed_contents_result_list_to_list
  (function_parameter : packed_contents_result_list)
  : list packed_contents_result :=
  let 'Contents_result_list l_value := function_parameter in
  contents_result_list_to_list l_value.

Fixpoint packed_contents_result_list_of_list
  (function_parameter : list packed_contents_result)
  : Pervasives.result packed_contents_result_list string :=
  match function_parameter with
  | [] ⇒ Pervasives.Error "cannot decode empty operation result"
  | cons (Contents_result o_value) [] ⇒
    Pervasives.Ok (Contents_result_list (Single_result o_value))
  | cons (Contents_result o_value) os ⇒
    let? 'Contents_result_list os := packed_contents_result_list_of_list os in
    match (o_value, os) with
    | (Manager_operation_result _, Single_result (Manager_operation_result _))
      ⇒ Pervasives.Ok (Contents_result_list (Cons_result o_value os))
    | (Manager_operation_result _, Cons_result _ _) ⇒
      Pervasives.Ok (Contents_result_list (Cons_result o_value os))
    | _ ⇒ Pervasives.Error "cannot decode ill-formed operation result"
    end
  end.

Definition contents_result_list_encoding
  : Data_encoding.encoding packed_contents_result_list :=
  Data_encoding.def "operation.alpha.contents_list_result" None None
    (Data_encoding.conv_with_guard packed_contents_result_list_to_list
      packed_contents_result_list_of_list None
      (Data_encoding.list_value None contents_result_encoding)).

Inductive contents_and_result_list : Set :=
| Single_and_result :
  Alpha_context.contents → contents_result → contents_and_result_list
| Cons_and_result :
  Alpha_context.contents → contents_result → contents_and_result_list →
  contents_and_result_list.

Inductive packed_contents_and_result_list : Set :=
| Contents_and_result_list :
  contents_and_result_list → packed_contents_and_result_list.

Fixpoint contents_and_result_list_to_list
  (function_parameter : contents_and_result_list)
  : list packed_contents_and_result :=
  match function_parameter with
  | Single_and_result op res ⇒ [ Contents_and_result op res ]
  | Cons_and_result op res rest ⇒
    cons (Contents_and_result op res) (contents_and_result_list_to_list rest)
  end.

Definition packed_contents_and_result_list_to_list
  (function_parameter : packed_contents_and_result_list)
  : list packed_contents_and_result :=
  let 'Contents_and_result_list l_value := function_parameter in
  contents_and_result_list_to_list l_value.

Fixpoint packed_contents_and_result_list_of_list
  (function_parameter : list packed_contents_and_result)
  : Pervasives.result packed_contents_and_result_list string :=
  match function_parameter with
  | [] ⇒ Pervasives.Error "cannot decode empty combined operation result"
  | cons (Contents_and_result op res) [] ⇒
    Pervasives.Ok (Contents_and_result_list (Single_and_result op res))
  | cons (Contents_and_result op res) rest ⇒
    let? 'Contents_and_result_list rest :=
      packed_contents_and_result_list_of_list rest in
    match (op, rest) with
    |
      (Alpha_context.Manager_operation _,
        Single_and_result (Alpha_context.Manager_operation _) _) ⇒
      Pervasives.Ok (Contents_and_result_list (Cons_and_result op res rest))
    | (Alpha_context.Manager_operation _, Cons_and_result _ _ _) ⇒
      Pervasives.Ok (Contents_and_result_list (Cons_and_result op res rest))
    | _ ⇒ Pervasives.Error "cannot decode ill-formed combined operation result"
    end
  end.

Definition contents_and_result_list_encoding
  : Data_encoding.encoding packed_contents_and_result_list :=
  Data_encoding.conv_with_guard packed_contents_and_result_list_to_list
    packed_contents_and_result_list_of_list None
    (Data_encoding._Variable.list_value None contents_and_result_encoding).

Module operation_metadata.
  Record record : Set := Build {
    contents : contents_result_list;
  }.
  Definition with_contents contents (r : record) :=
    Build contents.
End operation_metadata.
Definition operation_metadata := operation_metadata.record.

Inductive packed_operation_metadata : Set :=
| Operation_metadata : operation_metadata → packed_operation_metadata
| No_operation_metadata : packed_operation_metadata.

Definition operation_metadata_encoding
  : Data_encoding.encoding packed_operation_metadata :=
  Data_encoding.def "operation.alpha.result" None None
    (Data_encoding.union None
      [
        Data_encoding.case_value "Operation_metadata" None (Data_encoding.Tag 0)
          contents_result_list_encoding
          (fun (function_parameter : packed_operation_metadata) ⇒
            match function_parameter with
            |
              Operation_metadata {|
                operation_metadata.contents := contents
                  |} ⇒ Some (Contents_result_list contents)
            | _ ⇒ None
            end)
          (fun (function_parameter : packed_contents_result_list) ⇒
            let 'Contents_result_list contents := function_parameter in
            Operation_metadata
              {| operation_metadata.contents := contents; |});
        Data_encoding.case_value "No_operation_metadata" None
          (Data_encoding.Tag 1) Data_encoding.empty
          (fun (function_parameter : packed_operation_metadata) ⇒
            match function_parameter with
            | No_operation_metadata ⇒ Some tt
            | _ ⇒ None
            end)
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            No_operation_metadata)
      ]).

Definition kind_equal (op : Alpha_context.contents) (res : contents_result)
  : option eq :=
  match (op, res) with
  | (Alpha_context.Endorsement _, Endorsement_result _) ⇒ Some Eq
  | (Alpha_context.Endorsement _, _) ⇒ None
  | (Alpha_context.Preendorsement _, Preendorsement_result _) ⇒ Some Eq
  | (Alpha_context.Preendorsement _, _) ⇒ None
  | (Alpha_context.Dal_attestation _, Dal_attestation_result _) ⇒ Some Eq
  | (Alpha_context.Dal_attestation _, _) ⇒ None
  | (Alpha_context.Seed_nonce_revelation _, Seed_nonce_revelation_result _) ⇒
    Some Eq
  | (Alpha_context.Seed_nonce_revelation _, _) ⇒ None
  | (Alpha_context.Vdf_revelation _, Vdf_revelation_result _) ⇒ Some Eq
  | (Alpha_context.Vdf_revelation _, _) ⇒ None
  |
    (Alpha_context.Double_preendorsement_evidence _,
      Double_preendorsement_evidence_result _) ⇒ Some Eq
  | (Alpha_context.Double_preendorsement_evidence _, _) ⇒ None
  |
    (Alpha_context.Double_endorsement_evidence _,
      Double_endorsement_evidence_result _) ⇒ Some Eq
  | (Alpha_context.Double_endorsement_evidence _, _) ⇒ None
  | (Alpha_context.Double_baking_evidence _, Double_baking_evidence_result _) ⇒
    Some Eq
  | (Alpha_context.Double_baking_evidence _, _) ⇒ None
  | (Alpha_context.Activate_account _, Activate_account_result _) ⇒ Some Eq
  | (Alpha_context.Activate_account _, _) ⇒ None
  | (Alpha_context.Proposals _, Proposals_result) ⇒ Some Eq
  | (Alpha_context.Proposals _, _) ⇒ None
  | (Alpha_context.Ballot _, Ballot_result) ⇒ Some Eq
  | (Alpha_context.Ballot _, _) ⇒ None
  | (Alpha_context.Drain_delegate _, Drain_delegate_result _) ⇒ Some Eq
  | (Alpha_context.Drain_delegate _, _) ⇒ None
  | (Alpha_context.Failing_noop _, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation := Alpha_context.Reveal _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied applied
          |}) ⇒
    let applied := cast successful_manager_operation_result applied in
    match applied with
    | Reveal_result _ ⇒ Some Eq
    | _ ⇒ None
    end
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation := Alpha_context.Reveal _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked applied _
          |}) ⇒
    let applied := cast successful_manager_operation_result applied in
    match applied with
    | Reveal_result _ ⇒ Some Eq
    | _ ⇒ None
    end
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation := Alpha_context.Reveal _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed Alpha_context.Kind.Reveal_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation := Alpha_context.Reveal _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped Alpha_context.Kind.Reveal_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation := Alpha_context.Reveal _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transaction _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Transaction_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transaction _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Transaction_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transaction _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Transaction_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transaction _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Transaction_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transaction _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Origination_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Origination_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Origination_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Origination_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Origination _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Delegation _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Delegation_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Delegation _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Delegation_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Delegation _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Delegation_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Delegation _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Delegation_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Delegation _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Update_consensus_key _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Update_consensus_key_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Update_consensus_key _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Update_consensus_key_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Update_consensus_key _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Update_consensus_key_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Update_consensus_key _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Update_consensus_key_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Update_consensus_key _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Register_global_constant _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Register_global_constant_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Register_global_constant _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Register_global_constant_result _)
            _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Register_global_constant _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Register_global_constant_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Register_global_constant _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Register_global_constant_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Register_global_constant _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Set_deposits_limit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Set_deposits_limit_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Set_deposits_limit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Set_deposits_limit_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Set_deposits_limit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Set_deposits_limit_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Set_deposits_limit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Set_deposits_limit_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Set_deposits_limit _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Increase_paid_storage _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Increase_paid_storage_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Increase_paid_storage _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Increase_paid_storage_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Increase_paid_storage _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Increase_paid_storage_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Increase_paid_storage _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Increase_paid_storage_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Increase_paid_storage _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_origination
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_origination_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_origination
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Tx_rollup_origination_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_origination
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_origination_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_origination
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_origination_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_origination
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_submit_batch _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_submit_batch_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_submit_batch _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Tx_rollup_submit_batch_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_submit_batch _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_submit_batch _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_submit_batch _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_commit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_commit_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_commit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Tx_rollup_commit_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_commit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_commit_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_commit _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_commit_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_commit _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_return_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_return_bond_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_return_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Tx_rollup_return_bond_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_return_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_return_bond_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_return_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_return_bond_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_return_bond _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_recover_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_recover_bond_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_recover_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_recover_bond_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_recover_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_recover_bond _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_recover_bond _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_finalize_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied
            (Tx_rollup_finalize_commitment_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_finalize_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked
            (Tx_rollup_finalize_commitment_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_finalize_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind
            _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_finalize_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_finalize_commitment _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_remove_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_remove_commitment_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_remove_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked
            (Tx_rollup_remove_commitment_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_remove_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_remove_commitment _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_remove_commitment _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_rejection _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_rejection_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_rejection _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Tx_rollup_rejection_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_rejection _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_rejection_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_rejection _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_rejection_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_rejection _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_dispatch_tickets _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Tx_rollup_dispatch_tickets_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_dispatch_tickets _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked
            (Tx_rollup_dispatch_tickets_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_dispatch_tickets _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_dispatch_tickets _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Tx_rollup_dispatch_tickets _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transfer_ticket _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Transfer_ticket_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transfer_ticket _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Transfer_ticket_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transfer_ticket _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Transfer_ticket_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transfer_ticket _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Transfer_ticket_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Transfer_ticket _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Dal_publish_slot_header _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Dal_publish_slot_header_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Dal_publish_slot_header _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Dal_publish_slot_header_result _)
            _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Dal_publish_slot_header _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Dal_publish_slot_header_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Dal_publish_slot_header _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Dal_publish_slot_header_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Dal_publish_slot_header _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_originate _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_originate_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_originate _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_originate_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_originate _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_originate_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_originate _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_originate_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_originate _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_add_messages _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_add_messages_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_add_messages _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_add_messages_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_add_messages _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_add_messages_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_add_messages _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_add_messages_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_add_messages _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_cement _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_cement_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_cement _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_cement_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_cement _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_cement_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_cement _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_cement_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_cement _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_publish_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_publish_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_publish_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_publish_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_publish _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_refute _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_refute_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_refute _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_refute_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_refute _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_refute_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_refute _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_refute_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_refute _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_timeout _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Sc_rollup_timeout_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_timeout _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Sc_rollup_timeout_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_timeout _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_timeout_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_timeout _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_timeout_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_timeout _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_execute_outbox_message _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied
            (Sc_rollup_execute_outbox_message_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_execute_outbox_message _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked
            (Sc_rollup_execute_outbox_message_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_execute_outbox_message _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind
            _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_execute_outbox_message _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Sc_rollup_execute_outbox_message _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Zk_rollup_origination_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Zk_rollup_origination_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Zk_rollup_origination_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_origination _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Zk_rollup_origination_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_origination _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Zk_rollup_publish_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Zk_rollup_publish_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Zk_rollup_publish_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_publish _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Zk_rollup_publish_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_publish _
        |}, _) ⇒ None
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_update _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Applied (Zk_rollup_update_result _)
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_update _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Backtracked (Zk_rollup_update_result _) _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_update _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Failed
            Alpha_context.Kind.Zk_rollup_update_manager_kind _
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_update _
        |},
      Manager_operation_result {|
        contents_result.Manager_operation_result.operation_result :=
          Apply_operation_result.Skipped
            Alpha_context.Kind.Zk_rollup_update_manager_kind
          |}) ⇒ Some Eq
  |
    (Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.operation :=
        Alpha_context.Zk_rollup_update _
        |}, _) ⇒ None
  end.

Fixpoint kind_equal_list
  (contents : Alpha_context.contents_list) (res : contents_result_list)
  : option eq :=
  match (contents, res) with
  | (Alpha_context.Single op, Single_result res) ⇒
    match kind_equal op res with
    | None ⇒ None
    | Some Eq ⇒ Some Eq
    end
  | (Alpha_context.Cons op ops, Cons_result res ress) ⇒
    match kind_equal op res with
    | None ⇒ None
    | Some Eq ⇒
      match kind_equal_list ops ress with
      | None ⇒ None
      | Some Eq ⇒ Some Eq
      end
    end
  | _ ⇒ None
  end.

Fixpoint pack_contents_list
  (contents : Alpha_context.contents_list) (res : contents_result_list)
  : contents_and_result_list :=
  match (contents, res) with
  | (Alpha_context.Single op, Single_result res) ⇒ Single_and_result op res
  | (Alpha_context.Cons op ops, Cons_result res ress) ⇒
    Cons_and_result op res (pack_contents_list ops ress)
  | _ ⇒ unreachable_gadt_branch
  end.

Fixpoint unpack_contents_list (function_parameter : contents_and_result_list)
  : Alpha_context.contents_list × contents_result_list :=
  match function_parameter with
  | Single_and_result op res ⇒ ((Alpha_context.Single op), (Single_result res))
  | Cons_and_result op res rest ⇒
    let '(ops, ress) := unpack_contents_list rest in
    ((Alpha_context.Cons op ops), (Cons_result res ress))
  end.

Definition operation_data_and_metadata_encoding
  : Data_encoding.encoding
    (Alpha_context.packed_protocol_data × packed_operation_metadata) :=
  Data_encoding.def "operation.alpha.operation_with_metadata" None None
    (Data_encoding.union None
      [
        Data_encoding.case_value "Operation_with_metadata" None
          (Data_encoding.Tag 0)
          (Data_encoding.obj2
            (Data_encoding.req None None "contents"
              (Data_encoding.dynamic_size None
                contents_and_result_list_encoding))
            (Data_encoding.opt None None "signature" Signature.encoding))
          (fun (function_parameter :
            Alpha_context.packed_protocol_data ×
              packed_operation_metadata) ⇒
            match function_parameter with
            | (Alpha_context.Operation_data _, No_operation_metadata) ⇒
              None
            | (Alpha_context.Operation_data op, Operation_metadata res)
              ⇒
              match
                kind_equal_list
                  op.(Alpha_context.protocol_data.contents)
                  res.(operation_metadata.contents) with
              | None ⇒
                Pervasives.failwith
                  "cannot decode inconsistent combined operation result"
              | Some Eq ⇒
                Some
                  ((Contents_and_result_list
                    (pack_contents_list
                      op.(Alpha_context.protocol_data.contents)
                      res.(operation_metadata.contents))),
                    op.(Alpha_context.protocol_data.signature))
              end
            end)
          (fun (function_parameter :
            packed_contents_and_result_list × option Signature.t) ⇒
            let '(Contents_and_result_list contents, signature) :=
              function_parameter in
            let '(op_contents, res_contents) :=
              unpack_contents_list contents in
            ((Alpha_context.Operation_data
              {|
                Alpha_context.protocol_data.contents :=
                  op_contents;
                Alpha_context.protocol_data.signature :=
                  signature; |}),
              (Operation_metadata
                {| operation_metadata.contents := res_contents;
                  |})));
        Data_encoding.case_value "Operation_without_metadata" None
          (Data_encoding.Tag 1)
          (Data_encoding.obj2
            (Data_encoding.req None None "contents"
              (Data_encoding.dynamic_size None
                Alpha_context.Operation.contents_list_encoding))
            (Data_encoding.opt None None "signature" Signature.encoding))
          (fun (function_parameter :
            Alpha_context.packed_protocol_data ×
              packed_operation_metadata) ⇒
            match function_parameter with
            | (Alpha_context.Operation_data op, No_operation_metadata)
              ⇒
              Some
                ((Alpha_context.Contents_list
                  op.(Alpha_context.protocol_data.contents)),
                  op.(Alpha_context.protocol_data.signature))
            | (Alpha_context.Operation_data _, Operation_metadata _) ⇒
              None
            end)
          (fun (function_parameter :
            Alpha_context.packed_contents_list × option Signature.t) ⇒
            let '(Alpha_context.Contents_list contents, signature) :=
              function_parameter in
            ((Alpha_context.Operation_data
              {| Alpha_context.protocol_data.contents := contents;
                Alpha_context.protocol_data.signature :=
                  signature; |}), No_operation_metadata))
      ]).

Module block_metadata.
  Record record : Set := Build {
    proposer : Alpha_context.Consensus_key.t;
    baker : Alpha_context.Consensus_key.t;
    level_info : Alpha_context.Level.t;
    voting_period_info : Alpha_context.Voting_period.info;
    nonce_hash : option Nonce_hash.t;
    consumed_gas : Alpha_context.Gas.Arith.fp;
    deactivated : list Signature.public_key_hash;
    balance_updates : Alpha_context.Receipt.balance_updates;
    liquidity_baking_toggle_ema : Alpha_context.Liquidity_baking.Toggle_EMA.t;
    implicit_operations_results :
      list packed_successful_manager_operation_result;
    dal_attestation : option Alpha_context.Dal.Attestation.t;
  }.
  Definition with_proposer proposer (r : record) :=
    Build proposer r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_baker baker (r : record) :=
    Build r.(proposer) baker r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_level_info level_info (r : record) :=
    Build r.(proposer) r.(baker) level_info r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_voting_period_info voting_period_info (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) voting_period_info
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_nonce_hash nonce_hash (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      nonce_hash r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_consumed_gas consumed_gas (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) consumed_gas r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_deactivated deactivated (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) deactivated r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_balance_updates balance_updates (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) balance_updates
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_liquidity_baking_toggle_ema liquidity_baking_toggle_ema
    (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      liquidity_baking_toggle_ema r.(implicit_operations_results)
      r.(dal_attestation).
  Definition with_implicit_operations_results implicit_operations_results
    (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) implicit_operations_results
      r.(dal_attestation).
  Definition with_dal_attestation dal_attestation (r : record) :=
    Build r.(proposer) r.(baker) r.(level_info) r.(voting_period_info)
      r.(nonce_hash) r.(consumed_gas) r.(deactivated) r.(balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results)
      dal_attestation.
End block_metadata.
Definition block_metadata := block_metadata.record.

Definition block_metadata_encoding : Data_encoding.encoding block_metadata :=
  Data_encoding.def "block_header.alpha.metadata" None None
    (Data_encoding.conv
      (fun (function_parameter : block_metadata) ⇒
        let '{|
          block_metadata.proposer := {|
            Delegate_consensus_key.t.delegate := proposer;
              Delegate_consensus_key.t.consensus_pkh :=
                proposer_active_key
              |};
            block_metadata.baker := {|
              Delegate_consensus_key.t.delegate := baker;
                Delegate_consensus_key.t.consensus_pkh :=
                  baker_active_key
                |};
            block_metadata.level_info := level_info;
            block_metadata.voting_period_info := voting_period_info;
            block_metadata.nonce_hash := nonce_hash;
            block_metadata.consumed_gas := consumed_gas;
            block_metadata.deactivated := deactivated;
            block_metadata.balance_updates := balance_updates;
            block_metadata.liquidity_baking_toggle_ema :=
              liquidity_baking_toggle_ema;
            block_metadata.implicit_operations_results :=
              implicit_operations_results;
            block_metadata.dal_attestation := dal_attestation
            |} := function_parameter in
        ((proposer, baker, level_info, voting_period_info, nonce_hash,
          deactivated, balance_updates, liquidity_baking_toggle_ema,
          implicit_operations_results),
          (proposer_active_key, baker_active_key, consumed_gas, dal_attestation)))
      (fun (function_parameter :
        (Signature.public_key_hash × Signature.public_key_hash ×
          Alpha_context.Level.t × Alpha_context.Voting_period.info ×
          option Nonce_hash.t × list Signature.public_key_hash ×
          Alpha_context.Receipt.balance_updates ×
          Alpha_context.Liquidity_baking.Toggle_EMA.t ×
          list packed_successful_manager_operation_result) ×
          (Signature.public_key_hash × Signature.public_key_hash ×
            Alpha_context.Gas.Arith.fp × option Alpha_context.Dal.Attestation.t))
        ⇒
        let
          '((proposer, baker, level_info, voting_period_info, nonce_hash,
            deactivated, balance_updates, liquidity_baking_toggle_ema,
            implicit_operations_results),
            (proposer_active_key, baker_active_key, consumed_gas,
              dal_attestation)) := function_parameter in
        {|
          block_metadata.proposer :=
            {| Delegate_consensus_key.t.delegate := proposer;
              Delegate_consensus_key.t.consensus_pkh := proposer_active_key; |};
          block_metadata.baker :=
            {| Delegate_consensus_key.t.delegate := baker;
              Delegate_consensus_key.t.consensus_pkh := baker_active_key; |};
          block_metadata.level_info := level_info;
          block_metadata.voting_period_info := voting_period_info;
          block_metadata.nonce_hash := nonce_hash;
          block_metadata.consumed_gas := consumed_gas;
          block_metadata.deactivated := deactivated;
          block_metadata.balance_updates := balance_updates;
          block_metadata.liquidity_baking_toggle_ema :=
            liquidity_baking_toggle_ema;
          block_metadata.implicit_operations_results :=
            implicit_operations_results;
          block_metadata.dal_attestation := dal_attestation; |}) None
      (Data_encoding.merge_objs
        (Data_encoding.obj9
          (Data_encoding.req None None "proposer"
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
          (Data_encoding.req None None "baker"
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
          (Data_encoding.req None None "level_info" Alpha_context.Level.encoding)
          (Data_encoding.req None None "voting_period_info"
            Alpha_context.Voting_period.info_encoding)
          (Data_encoding.req None None "nonce_hash"
            (Data_encoding.option_value Nonce_hash.encoding))
          (Data_encoding.req None None "deactivated"
            (Data_encoding.list_value None
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
          (Data_encoding.dft None None "balance_updates"
            Alpha_context.Receipt.balance_updates_encoding nil)
          (Data_encoding.req None None "liquidity_baking_toggle_ema"
            Alpha_context.Liquidity_baking.Toggle_EMA.encoding)
          (Data_encoding.req None None "implicit_operations_results"
            (Data_encoding.list_value None
              successful_manager_operation_result_encoding)))
        (Data_encoding.obj4
          (Data_encoding.req None None "proposer_consensus_key"
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
          (Data_encoding.req None None "baker_consensus_key"
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
          (Data_encoding.req None None "consumed_milligas"
            Alpha_context.Gas.Arith.n_fp_encoding)
          (Data_encoding.varopt None None "dal_attestation"
            Alpha_context.Dal.Attestation.encoding)))).