🎛️ Constants_services.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_services.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_repr.
Module S.
Lemma errors_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Constants_services.S.errors.
Proof.
RPC_service.rpc_auto.
Qed.
Lemma all_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Constants_repr.Valid.t
Constants_services.S.all.
Proof.
RPC_service.rpc_auto.
Qed.
End S.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_services.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_repr.
Module S.
Lemma errors_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
Constants_services.S.errors.
Proof.
RPC_service.rpc_auto.
Qed.
Lemma all_is_valid
: RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Constants_repr.Valid.t
Constants_services.S.all.
Proof.
RPC_service.rpc_auto.
Qed.
End S.