found LJ icon of the day

[substitute]

Comments

[mrsgreer.livejournal.com]

d/dx*int(f(x))dx = f(x)

[substitute.livejournal.com]

bluh bluh BLUH!

And...

[mrhinelander.livejournal.com]

and int [f(x)dx] = ?

It equals COUNT, goddammit.

[dr-strych9.livejournal.com]

Γ ⊢ ν(α ∈ σ) M : τ & α ∉ ftv(τ)

[substitute.livejournal.com]

That's all geek to me.

[etb.livejournal.com]

I don't think that's well-formed, not even in the ⊢WTF system.

[dr-strych9.livejournal.com]

If it helps, 'ftv' is an abbreviation for "free type variable."

[etb.livejournal.com]

...and next you'll be telling me that Γ is a set of typing assumptions, M is a term and τ is a type, but I don't know what that & is doing in there.

[dr-strych9.livejournal.com]

Yeah, that is one of the problems when you're looking at that shit in a paper and trying to figure out how to translate it into Twelf.

[etb.livejournal.com]

Anyway, I'm curious what type system that's from; that's a tough thing to Google (though I'm amused that I wrote one of the top hits for "ftv(τ)").

[dr-strych9.livejournal.com]

It's in here somewhere.

[sooz.livejournal.com]

cute galore.

when i was a little person i used to think the count was related to us counters :P