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?

Follow

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

Sign in to participate in the conversation
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.