Three Dollar Quill

All right, things are moving along with working with sums. I've "proven" the distributive law and the associative law.

Dafny was all like "yeah, that's obvious, you don't need to write anything in the lemma body".

Anyway, the stuff I did to set that up does not quite transfer to the commutative law, so I need to do some more planning.

...

Also, I need to figure out how correctness-checking a lemma with an empty body can be brittle. Like, what? What's left to optimize?

...

Okay, I actually was able to squeeze a bit of brittleness out by making the preconditions more explicit. But still not all the way.

Anyway, that's it. I don't have anything else in mind, and I need to think and plan some more. I'd also like to get off my laptop.

Good night.