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 👈
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
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
ty🅿️es
nthe
: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
these days i just use my main (@g) for everything sorry
Joined Oct 2020
