Skip to content

Draft: Merging list based devs

Germán Delbianco requested to merge germanD@ax-list-spec into master

Implement #5 (closed).

TASKS

  • Add split_at implementation and prove its specification.
  • Implement the mutually recursive [insert_list] and [insert_node].
  • Prove the specification for [insert_list]
  • Pack the external API and prove the specification.
  • Improve comments.

LEFTOVER [ ] Prove the interchange spec lemma

Edited by Germán Delbianco

Merge request reports