-
Jakob Botsch Nielsen authored
* Pull the functionality we need into a Containers.v file that takes care of including the proper implementations of fmaps and fsets. Additionally, this file defines notation/new names. * Stop using map/set notation for operations. This conflicts with lists/record-set and is generally a head-ache. * Switch to lists instead of AVL trees for the sets and maps. This allows us to prove (assuming proof irrelevance) what we need: FSet.of_list (FSet.elements x) = x. Prove this and the equivalent for fin maps. * Do not use program instances in Oak.v. We can do with instances which generate a lot less bloat.
5e814944