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).
producing
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.