Skip to content

Fix go_left_spec

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

We fix the bug in insert_overflow (See #12 (closed)). There is still a lemma to prove about the new go_left_spec difinition (but now we have defined the unit (soon PBT) to check the equivalence between the specs).

Edited by Germán Delbianco

Merge request reports