⛽ Gas_comparable_input_size.v

Simulations

See code, See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Gas_comparable_input_size.

Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

Definition t : Set := Gas_comparable_input_size.t.

(* TODO *)

A simulation of [size_of_comparable_value].

Parameter dep_size_of_comparable_value : ∀ (a : Ty.t), Ty.to_Set a → t.