@zwarich @tmyklebu So the "debugging" loop for me has been starting with an initial, usually coarse proof obligation that fails and subdividing it until it's clear what part it couldn't figure out on its own. Often the final, working proof obligation can be pretty coarse, so the subdivision process is often only for debugging and you can unwind it once you know what's going on.
=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social
=> View zwarich@hachyderm.io profile | View tmyklebu@mastodon.gamedev.place profile
text/geminiThis content has been proxied by September (ba2dc).