🐆 Tx_rollup_errors_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
The function [check_path_depth_is_valid] is valid
Lemma check_path_depth_is_valid
kind_value provided count_limit :
letP? x := Tx_rollup_errors_repr.check_path_depth
kind_value provided count_limit in
True.
Proof.
unfold Tx_rollup_errors_repr.check_path_depth.
unfold error_when; now step.
Qed.
kind_value provided count_limit :
letP? x := Tx_rollup_errors_repr.check_path_depth
kind_value provided count_limit in
True.
Proof.
unfold Tx_rollup_errors_repr.check_path_depth.
unfold error_when; now step.
Qed.