Skip to main content

🍬 Script_tc_errors.v


See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.

A type family used to represent the GADT [error_details].
Module Error_trace_family.
  Inductive t : Set :=
  | Error_trace : t
  | Inconsistent_types_fast_error : t.

  Definition to_Set (x : t) : Set :=
    match x with
    | Error_traceError_monad.trace Error_monad._error
    | Inconsistent_types_fast_error
End Error_trace_family.

A dependent version of the type [error_details].
Conversion from [dep_error_details] back to its original type.