Nils Anders Danielsson
Nils Anders Danielsson
> I think we can handle both concerns positively This sounds promising.
> Steps 2 and 3 will likely introduce some (perhaps significant) overhead Step 1 would make it harder to use `IntMap`s and `IntSet`s, but I guess that would be possible...
I don't follow you. Different files can belong to different projects.
> I don't follow you. Different files can belong to different projects. This was a reply to a comment made by @andreasabel. Was this comment deleted?
When working on this I realised a potential problem: ``` $ cat B.agda module A.B where $ agda -i.. B.agda B.agda:1,8-11 You tried to load B.agda which defines the module...
Another problem: If you refer to the module `A.B` using the path `dir/A/C/../B.agda`, then the root directory (used to search for `.agda-lib` files) obtained from `projectRoot` is currently `dir/A/C`. How...
I went with the last option above ("check that the path suffix is correct"), and for the previous comment I went with the second option ("Use `canonicalizePath` to avoid at...
I should perhaps note that I have hardly tested the Emacs mode at all, and I expect that something will not work properly. However, I don't want to spend time...
@jespercockx, you could use `--with-K --cubical`: ```agda {-# OPTIONS --with-K --cubical #-} open import Agda.Builtin.Cubical.Glue ```
> I'd be interested in taking a look at the unification problem on which the LHS unifier is slow. I linked to some code above.