💾 Storage_functors.v

Simulations

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage_functors.

Module INDEX.

Conversion to [Path_encoding.S].

  Definition to_Path_encoding_S {t : Set} {ipath : Set → Set}
    (x : Storage_functors.INDEX (t := t) (ipath := ipath)) :
    Path_encoding.S (t := t) := {|
    Path_encoding.S.to_path := x.(Storage_functors.INDEX.to_path);
    Path_encoding.S.of_path := x.(Storage_functors.INDEX.of_path);
    Path_encoding.S.path_length := x.(Storage_functors.INDEX.path_length);
  |}.
End INDEX.