🍃 RPC_answer.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Module stream.
Record record {next shutdown : Set} : Set := Build {
next : next;
shutdown : shutdown }.
Arguments record : clear implicits.
Definition with_next {t_next t_shutdown} next
(r : record t_next t_shutdown) :=
Build t_next t_shutdown next r.(shutdown).
Definition with_shutdown {t_next t_shutdown} shutdown
(r : record t_next t_shutdown) :=
Build t_next t_shutdown r.(next) shutdown.
End stream.
Definition stream_skeleton := stream.record.
Reserved Notation "'stream".
Inductive t (o : Set) : Set :=
| OkStream : 'stream o → t o
| Unauthorized : option (list Error_monad._error) → t o
| OkChunk : o → t o
| Error : option (list Error_monad._error) → t o
| Ok : o → t o
| Not_found : option (list Error_monad._error) → t o
| Forbidden : option (list Error_monad._error) → t o
| Created : option string → t o
| Conflict : option (list Error_monad._error) → t o
| No_content : t o
where "'stream" := (fun (t_a : Set) ⇒
stream_skeleton (unit → option t_a) (unit → unit)).
Definition stream := 'stream.
Arguments OkStream {_}.
Arguments Unauthorized {_}.
Arguments OkChunk {_}.
Arguments Error {_}.
Arguments Ok {_}.
Arguments Not_found {_}.
Arguments Forbidden {_}.
Arguments Created {_}.
Arguments Conflict {_}.
Arguments No_content {_}.
Parameter _return : ∀ {o : Set}, o → t o.
Parameter return_chunked : ∀ {o : Set}, o → t o.
Parameter return_stream : ∀ {o : Set}, stream o → t o.
Parameter not_found : ∀ {o : Set}, t o.
Parameter fail : ∀ {a : Set}, list Error_monad._error → t a.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Module stream.
Record record {next shutdown : Set} : Set := Build {
next : next;
shutdown : shutdown }.
Arguments record : clear implicits.
Definition with_next {t_next t_shutdown} next
(r : record t_next t_shutdown) :=
Build t_next t_shutdown next r.(shutdown).
Definition with_shutdown {t_next t_shutdown} shutdown
(r : record t_next t_shutdown) :=
Build t_next t_shutdown r.(next) shutdown.
End stream.
Definition stream_skeleton := stream.record.
Reserved Notation "'stream".
Inductive t (o : Set) : Set :=
| OkStream : 'stream o → t o
| Unauthorized : option (list Error_monad._error) → t o
| OkChunk : o → t o
| Error : option (list Error_monad._error) → t o
| Ok : o → t o
| Not_found : option (list Error_monad._error) → t o
| Forbidden : option (list Error_monad._error) → t o
| Created : option string → t o
| Conflict : option (list Error_monad._error) → t o
| No_content : t o
where "'stream" := (fun (t_a : Set) ⇒
stream_skeleton (unit → option t_a) (unit → unit)).
Definition stream := 'stream.
Arguments OkStream {_}.
Arguments Unauthorized {_}.
Arguments OkChunk {_}.
Arguments Error {_}.
Arguments Ok {_}.
Arguments Not_found {_}.
Arguments Forbidden {_}.
Arguments Created {_}.
Arguments Conflict {_}.
Arguments No_content {_}.
Parameter _return : ∀ {o : Set}, o → t o.
Parameter return_chunked : ∀ {o : Set}, o → t o.
Parameter return_stream : ∀ {o : Set}, stream o → t o.
Parameter not_found : ∀ {o : Set}, t o.
Parameter fail : ∀ {a : Set}, list Error_monad._error → t a.