I didn't like how I blasted through naturals and lists so instead I'm redoing them with "Tees" and adding the ugliest colours because I can

I like your funny words, magic man

re: Corpse Reviver

Doing some very insightful and thoughtful annotations

I just wanna `ϵ: ok` today

I just wanna `P: ok`

Seven-word horror story

A very important question for the PList

Really going in with this onion metaphor

Trees are like onions.

By transitivity, datatypes are like ogres

Today's mood
I really thought Sizes were just going to be inductives and that's that

what is this going on about
I'm very Jared, 19

How should I fix that second sentence? ⊡!A⊢Γ and !⊡!A⊢Γ imply each other (by maximality, as it says), I'm trying to figure out what the intent of "for then" was

Since when did I need a licence??

logic cube

Oh here's the rules I settled on
The first two "facts" are derivable by induction and the third one is basically a macro for a derivation where you stick those Ds where the ps are in your tree, but I'm not sure about the fourth fact or how it's proven
It makes sense that you can replace a formula by an equivalent one but idk how to get "inside" C to do the replacement
I suppose it must be some proof by induction too

I'm proud of the double pun in this one

Okay I don't get this fourth one
Like I can see why it's invalid because B is just a random arbitrary formula unrelated to A but I don't get why they decided to state this particular schema
Like ?? what's the point of stating it

Excuse me, ticks are sizes
(slides)

Show older

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.