Skip to content

complete the proof for encoding in tx_rollup_state_repr

Shubham Kumar requested to merge shubham@encoding_proof_tx_rollup_state_repr into master

This MR resolves https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/113 and proves the lemma for encoding in Tx_rollup_state_repr.v

Edited by Shubham Kumar

Merge request reports