Skip to content

Original overflowing implementation of singleton insert

Germán Delbianco requested to merge germanD@overflow-cleanup into master

Implements #4 (closed)

TODO

  • Prove insert_pow specification
  • Clear admitted overflow axiom in insert_overflow.v
  • Pack Specification
Edited by Germán Delbianco

Merge request reports