🏗️ Apply_operation_result.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Inductive operation_result (manager successful : Set) : Set :=
| Applied : successful → operation_result manager successful
| Backtracked :
successful → option (Error_monad.trace Error_monad._error) →
operation_result manager successful
| Failed :
manager → Error_monad.trace Error_monad._error →
operation_result manager successful
| Skipped : manager → operation_result manager successful.
Arguments Applied {_ _}.
Arguments Backtracked {_ _}.
Arguments Failed {_ _}.
Arguments Skipped {_ _}.
Definition error_encoding : Data_encoding.encoding Error_monad._error :=
(fun x_1 ⇒
Data_encoding.def "error" x_1
(Some
("The full list of RPC errors would be too long to include." ++
String.String "010"
("It is available at RPC `/errors` (GET)." ++
String.String "010"
"Errors specific to protocol Alpha have an id that starts with `proto.alpha`."))))
None
(Data_encoding.splitted
(Data_encoding.conv
(fun (err : Error_monad._error) ⇒
Data_encoding.Json.construct None Error_monad.error_encoding err)
(fun (json_value : Data_encoding.json) ⇒
Data_encoding.Json.destruct None Error_monad.error_encoding json_value)
None Data_encoding.json_value) Error_monad.error_encoding).
Definition trace_encoding
: Data_encoding.t (Error_monad.trace Error_monad._error) :=
Error_monad.make_trace_encoding error_encoding.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Inductive operation_result (manager successful : Set) : Set :=
| Applied : successful → operation_result manager successful
| Backtracked :
successful → option (Error_monad.trace Error_monad._error) →
operation_result manager successful
| Failed :
manager → Error_monad.trace Error_monad._error →
operation_result manager successful
| Skipped : manager → operation_result manager successful.
Arguments Applied {_ _}.
Arguments Backtracked {_ _}.
Arguments Failed {_ _}.
Arguments Skipped {_ _}.
Definition error_encoding : Data_encoding.encoding Error_monad._error :=
(fun x_1 ⇒
Data_encoding.def "error" x_1
(Some
("The full list of RPC errors would be too long to include." ++
String.String "010"
("It is available at RPC `/errors` (GET)." ++
String.String "010"
"Errors specific to protocol Alpha have an id that starts with `proto.alpha`."))))
None
(Data_encoding.splitted
(Data_encoding.conv
(fun (err : Error_monad._error) ⇒
Data_encoding.Json.construct None Error_monad.error_encoding err)
(fun (json_value : Data_encoding.json) ⇒
Data_encoding.Json.destruct None Error_monad.error_encoding json_value)
None Data_encoding.json_value) Error_monad.error_encoding).
Definition trace_encoding
: Data_encoding.t (Error_monad.trace Error_monad._error) :=
Error_monad.make_trace_encoding error_encoding.