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 users who like the study of programming languages, formal semantics, types, or linguistics.