pounce - Network

why are mathematicians like this

why are mathematicians like this

as of today, the halloy irc client supports soju.im/bouncer-networks. this means when connecting to a bouncer it can autodetect your irc...

as of today, the halloy irc client supports soju.im/bouncer-networks. this means when connecting to a bouncer it can autodetect your irc networks and their statuses, and connect you to each one! We are now one step closer to "zero configuration" irc clients which stay synced between all of your devices!

The proof of Theorem 1.1 depends on Zorn’s lemmalove how analysis textbooks always start with this right off the bat

The proof of Theorem 1.1 depends on Zorn’s lemma

love how analysis textbooks always start with this right off the bat

welp, the open source nvidia drivers work better than nouveau again

welp, the open source nvidia drivers work better than nouveau again

in particular im working on an irc client where strings should really be parameterized over one of 5 "comparison modes" (because...

in particular im working on an irc client where strings should really be parameterized over one of 5 "comparison modes" (because IRC has different case-based comparison depending on the decade of ircd you're using, and you can't change the Ord/Cmp of a type at runtime)

so really you want a connection to have a cmpMode: Mode, and every string held by the connection to be a IrcStr<cmpMode>

Actegories for the Working Amthematicianextremely good paper title

Actegories for the Working Amthematician

extremely good paper title

kinda wish that rust had dependent types

kinda wish that rust had dependent types

is there any reason to even have Set 0? why not just have everything be universe level polymorphic over a theory of universes and the...

is there any reason to even have Set 0? why not just have everything be universe level polymorphic over a theory of universes and the lsuc/lub operations

ah yes, the fundamental theorem of calculus. or as i've recently taken to calling it, integral_eq_sub_of_hasDeriv_right

ah yes, the fundamental theorem of calculus. or as i've recently taken to calling it, integral_eq_sub_of_hasDeriv_right

NonBinary Evaluation

NonBinary Evaluation

if bidirectional typechecking is so good why isn't there tridirectional typechecking

if bidirectional typechecking is so good why isn't there tridirectional typechecking

or bad lean for that matter. why can't i (<- comp) at any place in an expression? why does it have to be the only thing on a line in...

or bad lean for that matter. why can't i (<- comp) at any place in an expression? why does it have to be the only thing on a line in do notation

every time i write haskell it just feels like bad agda

every time i write haskell it just feels like bad agda

mods, sheafify her

mods, sheafify her

Content warning:lsp alternatives musingi think varlink is really cool and might be nice as a transport layer for an lsp alternative...

Content warning:lsp alternatives musing

i think varlink is really cool and might be nice as a transport layer for an lsp alternative protocol, but afaik it's currently only defined on linux

if you're forced to use UI elements as a glyphs in a font, you should have a way to switch fonts and then put them in a different font!...

if you're forced to use UI elements as a glyphs in a font, you should have a way to switch fonts and then put them in a different font! i should not be forced to download a specific font that supports your bad design

i hate nerdfonts i hate nerdfonts i hate nerdfontsarbitrary UI elements no longer need to be given codepoints in every font you use!!!!

i hate nerdfonts i hate nerdfonts i hate nerdfonts

arbitrary UI elements no longer need to be given codepoints in every font you use!!!!

god i hate the nvim plugin ecosystem

god i hate the nvim plugin ecosystem

me: open module‌: no.... IMPOSSIBLE.... how could you do this to me

me: open module
‌: no.... IMPOSSIBLE.... how could you do this to me

im at my kan limit

im at my kan limit