Diary 2024-06-29
Still safe to skip.
Still safe to skip.
Very safe to skip.
This is all a bit awkward to work with.
Insert regular expressions joke here.
This is going to get so brittle when I manage to express absolute convergence. Oh well.
Dafny, please tell me what's missing.
Poking some more at Dafny.
I wasn't expecting some of these issues, but in retrospect, I can't imagine what else the documentation would have meant.
Hooray for tooling!
Quick thoughts on the layouts... the "Relation" module should be separate, and all of the rest should be focused around "real-valued sums"...