🖼️ Raw_context_intf.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_context_intf.

Properties over the [TREE] signature.

Module TREE.

The equality of two trees.

  Module Eq.
    Import Proto_alpha.Raw_context_intf.TREE.

    Record t {t tree : Set}
      (T1 T2 : Raw_context_intf.TREE (t := t) (tree := tree)) : Prop := {
      mem x k : T1.(mem) x k = T2.(mem) x k;
      mem_tree x k : T1.(mem_tree) x k = T2.(mem_tree) x k;
      get x k : T1.(get) x k = T2.(get) x k;
      get_tree x k : T1.(get_tree) x k = T2.(get_tree) x k;
      find x k : T1.(find) x k = T2.(find) x k;
      find_tree x k : T1.(find_tree) x k = T2.(find_tree) x k;
      (* TODO: add more comparisons for other fields *)
      empty ctxt : T1.(empty) ctxt = T2.(empty) ctxt;
      to_value x : T1.(to_value) x = T2.(to_value) x;
    }.
  End Eq.
End TREE.