To answer a question people sometimes ask: https://www.type-driven.org.uk/edwinb/why-is-idris-2-so-much-faster-than-idris-1.html
In which I explain several bad design decisions I made several years ago...
Alternative wishlist course: HoTT. That's it, it's just teaching HoTT directly from the book
When I visited McGill I got to drop in on a course and that class was discussing a paper on temporal type theory and it was big confusing, but I think if I understood the logic part of it I could've more easily grasped the typey part of it
If I could wish up a course it'd probably be a logic/type theory course
Probably half lecture, half seminar style
Start with lectures on nonclassical logics (modal, linear, temporal, whatever) and then read the big papers (assuming there are any) that establish the corresponding type theories
I wonder if I can take grad courses outside of CS... I probably just have to ask
If I have to take eight (!) courses or whatever with a set amount of them for a "breadth" requirement I might as well take something I'm actually interested in, like quantum mechanics, instead of a random AI/ML course to arrange my timetable
Pity there are only so many PL courses to take
It's kind of hard to tell how many puzzle pieces you want to provide the reader with when writing a paper proof
I'm glad I don't need to meticulously put all the pieces together though, unlike a mechanized proof
The list is in a weird order because I typed them out in the order I followed the derivation tree in my head depth-first lol
There's a _≡˘⟨_⟩_ operator that does that, it applies `sym` to the proof
I wish `rewrite` could try applying either of the provided proof or its `sym` though, I can never remember which way `assoc` is defined
pleas... I just want to do some induction... why won't things load properly by themselfs...
Oh I love Agda input mode so much. I possess the power of all the Unicode symbols
They need an Agda Tutorial For Abosolute Dunces, because I have no idea how to do anything
also why does it take so long
and what do I do with the .agdai file
Sometimes, when I press the flat square buttons, the lights from the glowy rectangle look nicer than usual #WaterDrinker
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!