pounce @pounce@types.pl

i just want to do algebraic geometry without the algebra is that too much to ask

i don't want to read Hartshorne please don't make me ​

i had to see the dafny logo again today, so you do too

getting lean3 mathlib working in neovim was surprisingly easy

not as easy as lean4 for sure but almost as good (and not bad at all considering the LS is an npm program)

amazing visualization of exact sequences and complexes https://www.3blue1brown.com/blog/exact-sequence-picturebook

pounce: i think i don't understand tensors of R-modules as well as i should, i wonder how to think about this topologically
pounce 30 min later: ​ ​

i should email matt flatt to let him know im writing PL-parsing scheme in my free time
i think that would make him feel good

calculamebussy

​

why go to the proof exchange stack exchange when you can come to the agda irc channel
(please join or it will die)

this is also probably stopping nyan.network from stealing types emojis, given that i don't have ​ there yet

ah, authorized fetch, that makes sense i guess, but it makes all the emoji pickers less nice to use
https://github.com/iliana/emojos.in/pull/15

is it because we're using jortage?? it used to work before

hmmm https://emojos.in/types.pl doesn't work anymore

bruh why am i getting so many frqs this is the account i don't use

oh no, somebody at work activated my interests and i talked about operating systems and type theory for an hour