Three Dollar Quill

I did a bunch of admin work stuff today, and then played video games, so I haven't done a ton of work with the Dafny code. Instead of trying to rush into anything, I'm going to plan a little for later:

• IsTotalOrder seems like a generally useful predicate.
• ThereIsAMinimum seems like a special-purpose lemma, which should get bundled up as a private member of the module that provides...
• SumOver, which I would like to figure out some way to provide an equivalent ghost version of that doesn't need an ordering. (The trick is proving that the two versions are equivalent.)
• LessEqual is a basic helper predicate that bundles with some of the predicates below, but I wouldn't mind getting rid of it if I work out the proof I mention above.
• I've got a bunch of helper things that I don't know how generally useful they are: HasMinimum, and Minumum are needed for how I'm trying to define absolute convergence, but I don't know if anything else has reason to refer to them.
• IRHelper is only needed because InclusiveRange was having troubles; wait, can I define nested functions in Dafny, because that would be handy here. Either way, these together represent a single coherent concept that seems generally useful. (Part of that usefulness is that I couldn't be bothered to figure out the right number theory proof for "there are a finite number of integers between any two integers, and if your response to that is "that sounds like something that the set comprehension heuristics should give you for free", the answer to that is "somehow, not the way I was using them".)
• SetUntil is a helper for absolute convergence stuff, but it's probably needed as part of proving absolute convergence in any specific case.
• NonNegativeAtValues is a predicate needed for absolute convergence stuff; I'm not sure offhand that there's any use exposing it.
• Then, I've finally got three predicates with really unwieldy names; these build up to the idea of absolute convergence, and until I try actually establishing absolute convergence of basic series, I won't know how generally useful they are to refer to.

So, that works out to four-ish modules I want to break this stuff into:

• total order and anything related to that somehow
• finite sums
• inclusive ranges
• limits of absolutely convergent sums

And, with that, I'm going to call things done for now, and get ready for bed.

Good night.