Jason (jcreed) wrote,

Got up pretty early this morning without an alarm, namely about 5:45. Headed over to campus about 6:15. There was a steady, gentle rain then. No hurricaneishness yet.

The sound of nothing but wind in the trees outside my bedroom recalled pleasant memories.
Though I know I'll never lose affection
For people and things that went before
I know I'll often stop and think about them
In my life* I love you more...

Tried hacking on twelf stuff, but ran into a brick wall: my minimal example of an error I think I shouldn't be getting is
o : type.
token : o -> type.
always : {x:o} token x -> type.
%mode (always +X -D).
%block b : block {x:o} {d:token x}.
%worlds (b) (always X D).
%covers (always +X -D).

Coverage error --- missing cases:
{#b:{x:o} {d:token x}} {X1:token #b_x} |- always #b_x X1.

I mean, what the fuck? I thought the possibility of the instantiation X1 <- #b_d was the whole idea of this regular worlds mumbo-jumbo. Geoff, Andrew, anyone else, if you can manage to explain how I'm being dumb, I'd be eternally grateful.

*best. use of. IVminor chord. ever.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded