Possibly hot take: the “case splitting” approach to program development via interactive program synthesis from extremely specific types has all the same problems that modifying and checking in generated code does, and we all learned why that was a bad idea a long time ago.
Conversation
Replying to
I think this one of the reasons folks like to use tactics instead, but then those have their own issues... 🤔