Mastodon Feed
dysfun@treehouse.systems ("gaytabase") wrote:
you know, i'm not sure i've ever mentioned this, but most of my idris is written by the case split key binding in emacs. since a massive part of idris is just pattern matching, case split just generates a massive part of your code for you on command.
what's more, it's better at it than i am, it will update depended-upon matches for you correctly, which you'd otherwise get a separate error about and then be puzzled until you worked out what it was telling you.
so when you run into a coverage checker bug or similar, you often have to write idris yourself.
i know that sounds silly, but if you actually write idris, you're making your life harder than it needs to be because of all the things that case split accounts for. and losing the ability to generate it makes the process somewhat more tedious.
none of this requires an LLM of course. and i don't think case split really qualifies as the same sort of thing.