Talk:CPS conversion

Strange world declarations

Can anybody pinpoint the reason that Twelf requires these odd world and mode declarations? Is it a bug?  — Tom 7 17:51, 5 October 2006 (EDT)

Termination order backwards?

It seems that the documentation in the guide is the opposite of what is actually implemented. With the total declaration

%total (A B C D) 
          (tocpsv- A _ _) 
          (tocpsv+ B _ _) 
          (tocps- _ C _ _ _) 
          (tocps+ _ D _ _ _).

I can call tocps- from tocps+ on the same derivation. The documentation says the opposite: that earlier theorems can call later ones. (See mutual recursion in the User's Guide). Am I crazy?  — Tom 7 17:55, 5 October 2006 (EDT)

I was under the impression it was later theorems that can call earlier ones (at least that's how I've used it in the past). --DanielKLee 16:48, 6 October 2006 (EDT)

Twelf output

The Twelf output indicates a syntax error in the example. Yay technology. --DanielKLee 16:48, 6 October 2006 (EDT)

Yeah, I was gonna mention that fact at some point. — Rob (and his talk) 17:19, 6 October 2006 (EDT)

We owe Tom an apology, he writes brillant code; he included type information in his code that was not part of the signature. Which is exactly what <twelf noinclude="true"> is for. — Rob (and his talk) 23:08, 6 October 2006 (EDT)

Word.  — Tom 7 23:52, 8 October 2006 (EDT)

You should use <twelf noinclude="true" check="decl"> to link to a %solve that establishes those derivations too, perhaps? — Rob (and his talk) 23:59, 8 October 2006 (EDT)

I'm really just using the twelf tag here to display a term with syntax highlighting; I don't think it needs to be checked. (Actually, I think it would distract from what's actually important.)  — Tom 7 14:41, 9 October 2006 (EDT)