⛽ Gas_monad.v

Simulations

See code, See proofs, Gitlab , OCaml

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

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

Simulation of [record_trace_eval].

Definition dep_record_trace_eval {error_context a : Set} {error_trace}
  (error_details : Script_tc_errors.dep_error_details error_context error_trace)
  (f_value : error_context → _error)
  (m_value : t a (Script_tc_errors.Error_trace_family.to_Set error_trace))
  : t a (Script_tc_errors.Error_trace_family.to_Set error_trace).
Admitted.