also :cybre:​ 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

Show thread

timeline goes sideways, contexts are now triangles

wait shit those coq posts were 🌏

looking forward to getting sealioned by fosstodon users

also: since it is causing actual problems in real life, obviously coq should be renamed

its just a name for a piece software, who cares. why wouldn't you change it if it makes people's lives easier

⊢ Γ boosted

oh god the penis logo hellthread just goes on forever

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

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

⊢ Γ boosted

please enjoy this random uuid 

b95720be-71c0-4d7a-9aa0-b21c5edf08c5
Show older
types.pl

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