🍃 RPC_path.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.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).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.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).