Coding 2024-02-09
It's a little weird that this works, except that there's no reason it shouldn't.
It's a little weird that this works, except that there's no reason it shouldn't.
A potential victory in the fight against Dafny's syntax(!)
Pardon my extremely unmotivated notational choices.
I accomplished a quantity of things that I find somewhat surprising.
The whole setup still looks a little strange.
Life hack: write the bulk of the post like three months ago, and then, this is the important part, actually publish it.
Oh well, maybe tomorrow, but leaning towards not.
Question: is Dafny "of the belief" that the ghost version takes on a single value? Because, if so, why isn't the lemma "obvious", and if not, what the heck does any of this mean?
Extremely excited to rewrite my tasks.py file to run dafny verify path/to/dfyconfig.toml as much as possible.
Hoarding property definitions like a really weird dragon.