Skip to content

Lazy storage diff encodings

Shubham Kumar requested to merge shubham@lazy_storage_diff_encodings_proof into master

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

Merge request reports