Three Dollar Quill

I've picked Dafny back up, updated it, deleted some asserts that are no longer required, (continued to despair that some asserts are required specifically to avoid z3 going into an infinite loop), and reviewed some of the code I wrote however many months ago. Because I didn't comment anything at the time, I had to look over the code and remember what the heck I was trying to do with all of it. Before I write any more code, I want to make sure to document this stuff thoroughly, so if I put this down and pick it back up, I can get up to speed in minutes rather than hours. I also think it might make sense to have separate modules defining deterministic and non-deterministic sums, but I'm not sure about that. Like, in my head, non-deterministic sums have a simple definition and support most theorems, and then deterministic sums "automatically" convert as many of those theorems as possible into theorems that apply to "method" contexts.

I'll just end up confused if I move hastily here, so I'm going to keep thinking about this, and focus on documentation, as I said. For now, I need to get ready for bed.

Good night.