Skip to main content

🍃 RPC_path.v

Environment

Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.RPC_arg.

Parameter t : (prefix params : Set), Set.

Definition path (prefix params : Set) : Set := t prefix params.

Definition context (prefix : Set) : Set := path prefix prefix.

Parameter root_value : context unit.

Parameter open_root : {a : Set}, context a.

Parameter add_suffix : {params prefix : Set},
  path prefix params string path prefix params.

Parameter op_div : {params prefix : Set},
  path prefix params string path prefix params.

Parameter add_arg : {a params prefix : Set},
  path prefix params RPC_arg.t a path prefix (params × a).

Parameter op_divcolon : {a params prefix : Set},
  path prefix params RPC_arg.t a path prefix (params × a).

Parameter add_final_args : {a params prefix : Set},
  path prefix params RPC_arg.t a path prefix (params × list a).

Parameter op_divcolonstar : {a params prefix : Set},
  path prefix params RPC_arg.t a path prefix (params × list a).