Three Dollar Quill

"Hey, what if I handle finite sums as a simple function, since those don't need to worry about convergence tests?"

"Hey, why don't I make the baseline implementation use finite sets, for flexibility?"

"... I don't understand how to iterate over a set in Dafny, possibly because I'm now too tired to read the documentation properly."

"After writing that last line, I figured out where to look in the documentation, and now I kind of wish I hadn't?"

Okay, so, if I want to do all of this in a function, I need to extract an element via a bizarre sequence of glyphs, then set difference it out and recurse? At least I don't need to worry myself about tail recursion, since I'm not planning to execute this. I might do it anyway, just because it's not like I can make this any harder to grasp.

Anyway, I'm going to consider it a win that I worked out that much, and try to get ready for bed.

Good night.