Asher Frost
Asher Frost
@magnus-madsen fixed in #10791 and #10852
Note:, this is a cleaner version of an earlier proposal, #3630
There is no *need* for this, only a *desire* for it. However, at least personally, this feels far more elegant. In addition, the holes above, in the case that you...
No I discussed this in detail with @andrevidela previously. Ultimately, the conclusion reached was the fundamentally the purpose of "unique holes" is that of a hole that is to be...
This is currently failing due to pack having a internal dependency on Idris file structure, so this should be pulled ***before*** [the pack pr](https://github.com/stefan-hoeck/idris2-pack/pull/346)
> It looks like it also breaks idris2-lsp and katla. Fixed!
Made some updates to the description
> Working on https://github.com/idris-lang/Idris2/pull/3513 to move forward with coming updates Agreeed