| src/Proto_alpha/Proofs/Tx_rollup_withdraw_list_hash_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Seed_repr.v | ['Lemma nonce_encoding_is_valid', 'Lemma seed_state_hash_encoding_is_valid: Data_encoding.Valid.t State_hash.Valid.t Seed_repr.state_hash_encoding.', 'Lemma seed_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Vote_repr.v | ['Lemma ballot_encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Cycle_repr.v | ['Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Saturation_repr.v | ['Lemma z_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_state_repr.v | ['Lemma range_encoding_is_valid : Data_encoding.Valid.t range.Valid.t'] | [] |
| src/Proto_alpha/Proofs/Sapling_repr.v | ['Lemma transaction_encoding_is_valid :', 'Lemma diff_encoding_is_valid :', ' Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Script_repr.v | ['Lemma exprencoding_is_valid :', 'Lemma location_encoding_is_valid : Data_encoding.Valid.t (fun => True) Scriptrepr.location_encoding.', 'Lemma lazy_expr_encoding_is_valid : Data_encoding.Valid.t (fun => True) Scriptrepr.lazy_expr_encoding.', 'Lemma encoding_is_valid : Data_encoding.Valid.t (fun => True) Script_repr.encoding.'] | [] |
| src/Proto_alpha/Proofs/Receipt_repr.v | ['Lemma balance_encoding_is_valid :', 'Lemma balance_update_encoding_is_valid :', 'Lemma update_origin_encoding_is_valid :', 'Lemma balance_updates_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Apply_results.v | ['Lemma trace_encoding_is_valid :', ' Lemma internal_operation_result_encoding_is_valid :', ' Lemma successful_manager_operation_result_encoding_is_valid :', 'Lemma contents_result_list_encoding_is_valid :', 'Lemma contents_and_result_list_encoding_is_valid :', 'Lemma operation_metadata_encoding_is_valid :', 'Lemma operation_data_and_metadata_encoding_is_valid :', 'Lemma block_metadata_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_message_result_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_l2_proof.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_l2_address.v | [' Lemma encoding_is_valid : Data_encoding.Valid.t Indexable.Valid.t ', ' Lemma index_encoding_is_valid :', ' Lemma value_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Ticket_hash_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_repr.v | [' Lemma encoding_is_valid :', 'Lemma encoding_is_valid :', 'Lemma index_path_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_inbox_repr.v | [] | [' Lemma root_encoding_is_valid :', ' Lemma path_encoding_is_valid :', 'Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t'] |
| src/Proto_alpha/Proofs/Michelson_v1_primitives.v | ['Lemma prim_encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Voting_period_repr.v | ['Lemma kind_encoding_is_valid :', 'Lemma encoding_is_valid :', 'Lemma info_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Level_repr.v | ['Lemma encoding_is_valid :', 'Lemma cycle_era_encoding_is_valid :', 'Lemma cycle_eras_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Vote_storage.v | ['Lemma ballots_encoding_is_valid :', 'Lemma listings_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Constants_repr.v | ['Lemma ratio_encoding_is_valid', 'Lemma fixed_encoding_is_valid', 'Lemma parametric_encoding_is_valid', 'Lemma encoding_is_valid', ' Lemma delegate_selection_encoding_is_valid', ' Lemma parametric_encoding_is_valid '] | [] |
| src/Proto_alpha/Proofs/Parameters_repr.v | ['Lemma bootstrap_account_encoding_is_valid : ', 'Lemma bootstrap_contract_encoding_is_valid :', 'Lemma encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Script_expr_hash.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Alpha_services.v | [' Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Origination_nonce.v | ['Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Operation_repr.v | ['Lemma consensus_content_encoding_is_valid :', ' Lemma preendorsement_encoding_is_valid :', ' Lemma endorsement_encoding_is_valid :', ' Lemma manager_encoding_is_valid :', ' Lemma contents_list_encoding_is_valid :', ' Lemma optional_signature_encoding_is_valid :', ' Lemma protocol_data_encoding_is_valid :', ' Lemma operation_encoding_is_valid :', ' Lemma unsigned_operation_encoding_is_valid :', 'Lemma encoding_is_valid :', 'Lemma contents_encoding_is_valid :', 'Lemma contents_list_encoding_is_valid :', 'Lemma protocol_data_encoding_is_valid :', 'Lemma unsigned_operation_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Entrypoint_repr.v | ['Lemma simple_encoding_is_valid :', 'Lemma value_encoding_is_valid :', 'Lemma smart_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Script_typed_ir.v | [' Lemma encodingis_valid : Data_encoding.Valid.t (fun => True) encoding.'] | [] |
| src/Proto_alpha/Proofs/Contract_storage.v | [' Lemma item_encoding_is_valid', ' Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Period_repr.v | [' Lemma encoding_is_valid', 'Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Bond_id_repr.v | ['Lemma encoding_is_valid :', 'Lemma index_path_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Blinded_public_key_hash.v | ['Lemma encoding_is_valid :', 'Lemma activation_code_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Nonce_storage.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Contract_services.v | ['Lemma info_encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Sapling_storage.v | ['Lemma root_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Nonce_hash.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tez_repr.v | ['Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Tez_repr.encoding.'] | [] |
| src/Proto_alpha/Proofs/Liquidity_baking_repr.v | ['Lemma liquidity_baking_toggle_vote_encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Script_int_repr.v | ['Lemma z_encoding_is_valid : ', 'Lemma n_encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_withdraw_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_message_repr.v | ['Lemma depositencoding_is_valid : Data_encoding.Valid.t Deposit.Valid.t', 'Lemma batch_encoding_is_valid : Data_encoding.Valid.t (fun => True)', 'Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t'] | [] |
| src/Proto_alpha/Proofs/Bitset.v | ['Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Bitset.encoding.'] | [] |
| src/Proto_alpha/Proofs/State_hash.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Round_repr.v | ['Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Round_repr.encoding.', ' Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Destination_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Fitness_repr.v | ['Lemma encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Manager_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Slot_repr.v | ['Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Slot_repr.encoding.'] | [] |
| src/Proto_alpha/Proofs/Indexable.v | [] | ['Lemma encoding_is_valid {a : Set} (val_encoding : Data_encoding.t a) :'] |
| src/Proto_alpha/Proofs/Delegate_services.v | ['Lemma info_encoding_is_valid', 'Lemma participation_info_encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_commitment_repr.v | [' Lemma encoding_is_valid :', ' Lemma encoding_is_valid :', ' Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Raw_level_repr.v | ['Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Lazy_storage_kind.v | ['Lemma encoding_is_valid (y : Lazy_storage_kind.MakeId.FArgs) : ', 'Lemma big_map_alloc_encoding_is_valid : ', 'Lemma update_encoding_is_valid : ', 'Lemma updates_encoding_is_valid : ', 'Lemma sapling_state_alloc_encoding_is_valid : ', 'Lemma sapling_state_updates_encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Script_timestamp_repr.v | ['Lemma encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Commitment_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Contract_repr.v | ['Lemma encodingis_valid : Data_encoding.Valid.t (fun => True) Contract_repr.encoding.', 'Lemma index_path_encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Sapling_services.v | [' Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Sc_rollup_repr.v | [' Lemma encoding_is_valid :', ' Lemma encoding_is_valid :', ' Lemma encoding_is_valid :', 'Lemma encoding_is_valid :', 'Lemma index_path_encoding_is_valid :', ' Lemma encoding_is_valid'] | [] |
| src/Proto_alpha/Proofs/Sc_rollup_inbox_repr.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Block_header_repr.v | ['Lemma raw_encoding_is_valid :', 'Lemma shell_header_encoding_is_valid :', 'Lemma contents_encoding_is_valid :', 'Lemma protocol_data_encoding_is_valid :', 'Lemma unsigned_encoding_is_valid :', 'Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_l2_qty.v | [] | ['Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t'] |
| src/Proto_alpha/Proofs/Block_payload_hash.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Gas_limit_repr.v | [' Lemma z_integral_encoding_is_valid', ' Lemma n_integral_encoding_is_valid :', ' Lemma n_fp_encoding_is_valid :', 'Lemma S_z_encoding_is_valid :', 'Lemma Arith_z_fp_encoding_is_valid :', 'Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Gas_limit_repr.encoding.', 'Lemma cost_encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Migration_repr.v | ['Lemma origination_result_list_encoding_is_valid : '] | [] |
| src/Proto_alpha/Proofs/Contract_hash.v | ['Lemma encoding_is_valid :'] | [] |
| src/Proto_alpha/Proofs/Tx_rollup_reveal_repr.v | ['Lemma encoding_is_valid :'] | [] |