🏗️ Apply_operation_result.v

Translated OCaml

Gitlab , 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.