🍃 RPC_context.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Updater.
Definition t : Set := Updater.rpc_context.
Module simple.
Record record {pr : Set} : Set := Build {
call_proto_service0 :
∀ {q i o : Set},
RPC_service.t t t q i o → pr → q → i →
Error_monad.shell_tzresult o;
call_proto_service1 :
∀ {a q i o : Set},
RPC_service.t t (t × a) q i o → pr → a → q → i →
Error_monad.shell_tzresult o;
call_proto_service2 :
∀ {a b q i o : Set},
RPC_service.t t ((t × a) × b) q i o → pr → a → b → q → i →
Error_monad.shell_tzresult o;
call_proto_service3 :
∀ {a b c q i o : Set},
RPC_service.t t (((t × a) × b) × c) q i o → pr → a → b → c → q →
i → Error_monad.shell_tzresult o }.
Arguments record : clear implicits.
End simple.
Definition simple := simple.record.
Parameter make_call0 : ∀ {i o pr q : Set},
RPC_service.t t t q i o → simple pr → pr → q → i →
Error_monad.shell_tzresult o.
Parameter make_call1 : ∀ {a i o pr q : Set},
RPC_service.t t (t × a) q i o → simple pr → pr → a → q → i →
Error_monad.shell_tzresult o.
Parameter make_call2 : ∀ {a b i o pr q : Set},
RPC_service.t t ((t × a) × b) q i o → simple pr → pr → a → b → q →
i → Error_monad.shell_tzresult o.
Parameter make_call3 : ∀ {a b c i o pr q : Set},
RPC_service.t t (((t × a) × b) × c) q i o → simple pr → pr → a → b →
c → q → i → Error_monad.shell_tzresult o.
Parameter make_opt_call0 : ∀ {i o pr q : Set},
RPC_service.t t t q i o → simple pr → pr → q → i →
Error_monad.shell_tzresult (option o).
Parameter make_opt_call1 : ∀ {a i o pr q : Set},
RPC_service.t t (t × a) q i o → simple pr → pr → a → q → i →
Error_monad.shell_tzresult (option o).
Parameter make_opt_call2 : ∀ {a b i o pr q : Set},
RPC_service.t t ((t × a) × b) q i o → simple pr → pr → a → b → q →
i → Error_monad.shell_tzresult (option o).
Parameter make_opt_call3 : ∀ {a b c i o pr q : Set},
RPC_service.t t (((t × a) × b) × c) q i o → simple pr → pr → a → b →
c → q → i → Error_monad.shell_tzresult (option o).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Updater.
Definition t : Set := Updater.rpc_context.
Module simple.
Record record {pr : Set} : Set := Build {
call_proto_service0 :
∀ {q i o : Set},
RPC_service.t t t q i o → pr → q → i →
Error_monad.shell_tzresult o;
call_proto_service1 :
∀ {a q i o : Set},
RPC_service.t t (t × a) q i o → pr → a → q → i →
Error_monad.shell_tzresult o;
call_proto_service2 :
∀ {a b q i o : Set},
RPC_service.t t ((t × a) × b) q i o → pr → a → b → q → i →
Error_monad.shell_tzresult o;
call_proto_service3 :
∀ {a b c q i o : Set},
RPC_service.t t (((t × a) × b) × c) q i o → pr → a → b → c → q →
i → Error_monad.shell_tzresult o }.
Arguments record : clear implicits.
End simple.
Definition simple := simple.record.
Parameter make_call0 : ∀ {i o pr q : Set},
RPC_service.t t t q i o → simple pr → pr → q → i →
Error_monad.shell_tzresult o.
Parameter make_call1 : ∀ {a i o pr q : Set},
RPC_service.t t (t × a) q i o → simple pr → pr → a → q → i →
Error_monad.shell_tzresult o.
Parameter make_call2 : ∀ {a b i o pr q : Set},
RPC_service.t t ((t × a) × b) q i o → simple pr → pr → a → b → q →
i → Error_monad.shell_tzresult o.
Parameter make_call3 : ∀ {a b c i o pr q : Set},
RPC_service.t t (((t × a) × b) × c) q i o → simple pr → pr → a → b →
c → q → i → Error_monad.shell_tzresult o.
Parameter make_opt_call0 : ∀ {i o pr q : Set},
RPC_service.t t t q i o → simple pr → pr → q → i →
Error_monad.shell_tzresult (option o).
Parameter make_opt_call1 : ∀ {a i o pr q : Set},
RPC_service.t t (t × a) q i o → simple pr → pr → a → q → i →
Error_monad.shell_tzresult (option o).
Parameter make_opt_call2 : ∀ {a b i o pr q : Set},
RPC_service.t t ((t × a) × b) q i o → simple pr → pr → a → b → q →
i → Error_monad.shell_tzresult (option o).
Parameter make_opt_call3 : ∀ {a b c i o pr q : Set},
RPC_service.t t (((t × a) × b) × c) q i o → simple pr → pr → a → b →
c → q → i → Error_monad.shell_tzresult (option o).