Ugh, Coq keeps crashing on me. Apparently this proof just has too many goals. Not sure what to do about this... perhaps it's time to learn proof-by-reflection?


But then I'd have to come up with (at least partial) decision procedures, which sounds hard....

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.