Commit 2022-01-27 16:51 dd7b052b

feat: union-find data structure (#139) This was surprisingly intricate to get right, considering that the implementation in CLRS is only 11 lines for all the functions in the API put together. All the invariants here are used only to prove that accesses are in bounds and the link function terminates. The fact that (a.set ..).size is not defeq to a.size causes no end of headache. Here I've experimented with a UFModel ghost type, which has simpler defeqs based on Fin n -> A functions instead of lists