Pinned toot

📌​ i still check the local tl on here but i am too lazy to sort posts into different accounts so just follow my main if you're interested 👉 @g@cybre.space 👈

⊢ Γ boosted

please don't ask me what a type is, i have no idea

i have got to know what the fuck the use case is for datatypes in SizeUniv

📌​ i still check the local tl on here but i am too lazy to sort posts into different accounts so just follow my main if you're interested 👉 @g@cybre.space 👈

⊢ Γ boosted

didn't mean to make this a whole day poll

anyway the answer is 57%. excluding the equalities that are actually part of definitions, just the bullshit like instances of Proper and etc

Show thread

i have some coq code here. how much, by line count, do you think is just fucking around with setoids

when your straight friends use the right pronouns

⊢ Γ boosted

@axakatl type theory is figuring out what a pokemon is good against in matchups

lol making code fit in a mastodon column sucks. no idea if it actually does fit for everyone else either. lmao

weak1 : VarL m -> VarL (S m)
weak1 =
weak $
lteSuccRight $
reflexive {rel=LTE}
-- Data.Nat.lteSuccRight :
-- LTE n m -> LTE n (S m)
-- Control.Relation.reflexive :
-- Reflexive ty rel => rel x x

i feel like idris should be able to infer the rel argument to reflexive here from the type of lteSuccRight, but it can't. and it never can. what's up with that

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.