🍃 RPC_context.v

Environment

Gitlab

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).