Skip to main content

⛽ Gas_comparable_input_size.v

Simulations

See code, See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
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.