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

@g they never ask how is a type

it's just a little guy

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 👈

putStrLn "im gay"

⊢ Γ boosted

doing important language design work

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

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

greetings from setoid hell

when your straight friends use the right pronouns

ty🅿️es

nthe

⊢ Γ boosted

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

:wide_η:

boumderies,,,

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

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