🍃 RPC_service.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Module Valid.
Import RPC_service.t.
Record t {prefix params query input output : Set}
(domain_query : query → Prop)
(domain_input : input → Prop)
(domain_output : output → Prop)
(service : RPC_service.t prefix params query input output) : Prop := {
query_rpc : RPC_query.Valid.t domain_query service.(query_rpc);
input_encoding :
Data_encoding.Valid.t domain_input service.(input_encoding);
output_encoding :
Data_encoding.Valid.t domain_output service.(output_encoding);
}.
End Valid.
Ltac rpc_auto :=
constructor;
match goal with
| |- Data_encoding.Valid.t _ _ ⇒ Data_encoding.Valid.data_encoding_auto
| |- RPC_query.Valid.t _ _ ⇒ RPC_query.valid_auto
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Module Valid.
Import RPC_service.t.
Record t {prefix params query input output : Set}
(domain_query : query → Prop)
(domain_input : input → Prop)
(domain_output : output → Prop)
(service : RPC_service.t prefix params query input output) : Prop := {
query_rpc : RPC_query.Valid.t domain_query service.(query_rpc);
input_encoding :
Data_encoding.Valid.t domain_input service.(input_encoding);
output_encoding :
Data_encoding.Valid.t domain_output service.(output_encoding);
}.
End Valid.
Ltac rpc_auto :=
constructor;
match goal with
| |- Data_encoding.Valid.t _ _ ⇒ Data_encoding.Valid.data_encoding_auto
| |- RPC_query.Valid.t _ _ ⇒ RPC_query.valid_auto
end.