Lazy storage diff encodings
This MR closes https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/99
Although the proof contains proof for diff_encoding
while item_encoding
is axiomatized because the corresponding ocaml code is using gadts which is partially supported by coq-of-ocaml
.
Edited by Shubham Kumar