Skip to content

Map cleanup

Evan Marzion requested to merge map-cleanup into master

Addresses #124 (closed)

  • Completed proofs of find_add, find_update, and find_singleton
  • Overhauled lawful comparison and sortedness definitions, with many lemmas about these properties
  • Fixed _Set proofs and work on sensible typeclass structuring relating Map's and _Set's FArgs
Edited by Evan Marzion

Merge request reports