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....

@akhirsch I think Adam's advice is to build a bigger machine. If you have less than 1TB of RAM, how do you even Coq?

Sign in to participate in the conversation

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