👔 Manager_counter_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require Import TezosOfOCaml.Proto_alpha.Manager_counter_repr.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require Import TezosOfOCaml.Proto_alpha.Manager_counter_repr.
Module Valid.
Validity predicate for the [Z.t] type
in the [encoding_for_operation].
The [encoding_for_operation] encoding is valid
Lemma encoding_for_operation_is_valid :
Data_encoding.Valid.t Valid.t
Manager_counter_repr.encoding_for_operation.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x ?.
unfold Valid.t in H.
lia.
Qed.
#[global] Hint Resolve encoding_for_operation_is_valid : Data_encoding_db.
Data_encoding.Valid.t Valid.t
Manager_counter_repr.encoding_for_operation.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x ?.
unfold Valid.t in H.
lia.
Qed.
#[global] Hint Resolve encoding_for_operation_is_valid : Data_encoding_db.