⊢ Γ @g@types.pl

also ​ is having a bit of a slow morning. same, buddy

i saw someone mention 'glide typing' and was all wtf is that till i realised they were talking about an android keyboard

im reading the graded "fuck you, two dimensional context" modal type theory paper again

wait shit those coq posts were 🌏

looking forward to getting sealioned by fosstodon users

Vile. Repulsive. Disgusting.

its kinda weird how usually when people say "x is admissible" they mean "x can be proven" but in coq you say "Admitted." to specifically mean "i was unable¹ to prove this"

¹or couldn't be arsed

... + admit

Ltac please := lra + lia + field + ring + congruence + tauto.