3 ms·
The rest of his thread: >That probably sounds like it'd be annoying, but it took about 20 seconds to fix, and it's not as annoying as forgetting the feature is
by rsstack 6y ago
The rest of his thread:
>That probably sounds like it'd be annoying, but it took about 20 seconds to fix, and it's not as annoying as forgetting the feature is there.
>We always give talks that show off the fancy stuff. Maybe one day I should collect together all these everyday little things and talk about them instead.
>I would need some new jokes to keep it interesting, I suppose.
- ricree 6y agoSpeaking of "rest of", this is the file in question: https://github.com/idris-lang/Idris2/blob/master/src/Idris/Env.idr#L47 https://github.com/idris-lang/Idris2/blob/master/src/Idris/E...