Skip to content

Vote proof

Basile Pesin requested to merge Vertmo/mi-cho-coq:vote-proof into master

Thanks to the proof of map extensionality (!15 (merged)), I was able to finish the proof of the vote contract.

WIP: I'm going to move all the small lemmas on map and comparable type to the appropriate files (they will probably be useful to prove other contracts).

Edited by Basile Pesin

Merge request reports