Talk:Debugging coverage errors

From The Twelf Project

When I have higher-order terms (in particular if I have a judgment that handles transitivity of higher-order contexts -- I can given an example) and do case analysis on them, I frequently get a nasty case of inactive splits AND nontermination. The only solution I have found is to split the metatheorem into two parts: one to handle the higher-order term in general and a second to do a case analysis between fixed terms. Boyland 09:31, 27 December 2009 (EST)