wen @cyrridven@computerfairi.es

Turns out the 2 year wait for your 2nd referral is enough time for them to lose your 1st referral, shrug, and just not refer you without telling you.

I am having feelings.

@lambdagrrl Yes, display logic, where all logical rules follow directly from polarity.

@lambdagrrl Yeah, there is :)

@lambdagrrl Oh, woops, did I mess that up? The branching rules were meant to be listed as interesting. Though the boring rules are actually the non-invertable rules, whereas the others are invertable, so there's a good argument for flipping the boring/interesting distinction.

@lambdagrrl The one looks boring, the other doesn't, but they both follow directly from the polarity of the connective, so I guess they're both kinda dull.

Sequent calculus talks about left and right rules. Is there terminology within sequent calculus for boring rules (L∧,R∨,L→) versus interesting rules (R∧,L∨,R→)?

Gotta say, very much a "do as I say, not as I do", 'cuz I use a *lot* of TeX packages, and I've never acknowledged their authors. Gonna give it a shot in the future! :)

This is from "Lambda terms for natural deduction, sequent calculus and cut elimination" by Henk Barendregt and Silvia Ghilezan [https://doi.org/10.1017/S0956796899003524]

Acknowledging the people who wrote your TeX macros is so wholesome, more people should do it!

@lambdagrrl she got distracted, sorry

@lambdagrrl tell that to my lack of impulse control

@lambdagrrl my mishaps are more of the "drops knife" or "dries knife" or "dances with knife" variety.

There's not enough cat pics on my account: this is Zaza, she likes to sleep on upright pillows.

"Oh, I need a different version of Agda for this project!"

*hits compile, walks away, forgets about project, and never comes back*

Right now I've got burns on my knee from cooking. ON MY KNEE!

Listen, I would love a really fancy knife for cooking, but I'm a clumsy bitch and I WOULD gut myself.

Woo, I got endorsed! I'm a real research now! *proud baby pose*