Draft: Merging list based devs
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