Skip to content

Compare: proof for Indexable.compare_values_is_valid

Guillaume Claret requested to merge guillaume-claret@compare-proof-example into master

Proof following the example of https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_string_repr/#compare_is_valid One modification to the Compare lemma was actually needed.

Merge request reports