🎛️ Constants_services.v

Proofs

See code, Gitlab , OCaml

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.