?

Log in

No account? Create an account
Arrrgh. - MrPutter: doing things the hard way, because it is there.
November 28th, 2005
04:01 am
[User Picture]

[Link]

Previous Entry Share Next Entry
Arrrgh.
So, hell. I just don't know any more. Does the following require collection on x, y and t; on x, y and t′; just on t and t′; or heck, on all four??

Le Sigh. It's way too late at night to be thinking about these things...

     z::Γ ⊢ t::Z     z::Γ, x::X, y::Y ⊢ t′::Q
     -----------------------------------------  X,Y ⊳ Z=X×Y
         z::Γ ⊢ (case t of (x,y) ↦ t′)::Q

Current Mood: crankycranky
Current Music: Soul Asylum -- Nothing to Write Home About
Tags: ,

(1 comment , Leave a comment)

Comments
 
[User Picture]
From:mrputter
Date:December 3rd, 2005 02:59 am (UTC)
(Link)
...and of course I'm an idiot. One collects on the sequents, not the terms...
Beware of Road Surprises Powered by LiveJournal.com