Nils Anders Danielsson
Nils Anders Danielsson
I tried to use the new implementation of "go-to-definition", but encountered error messages of the following form: ``` cl-no-applicable-method: No applicable method: xref-backend-definitions, agda2, "…" ```
> ``` > /bin/cp -p -f src/data/emacs-mode/*.el ~/.cabal/share/x86_64-osx-ghc-9.4.4/Agda-2.6.4/emacs-mode/ > ``` The directory can be obtained by using something like `dirname $(agda-mode locate)`. Note that Emacs (by default?) uses byte-compiled files,...
No one replied when I asked for feedback, and now I'm working on other things.
Possibly related: #1555.
I mentioned this bug in the user manual: https://github.com/agda/agda/blob/5f10da9394ea71faca00c5828df4bfdc147e99ca/doc/user-manual/tools/interface-files.rst?plain=1#L36-L39
I [asked](https://github.com/agda/agda/issues/4784#issuecomment-1287803484) a similar question for the following type: ```agda record R : Set₁ where field @0 A : Set x : A ``` I received an answer from @Saizan...
> I'm not sure how to interpret "it is OK to erase transports". The erasure function for Erased Cubical Agda contains the clause `|primTransp _ _ e| = |e|`. This...
> @pigworker also seems to agree, see the FUN-rule on p6 of https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf (I'm assuming that absence of a quantity means ω). That paper is not about cubical type theory....
> You are the one who used that phrasing earlier in this issue. I just wanted to make clear that I was not quoting but paraphrasing @Saizan. > This does...
I do not currently plan to continue working on this.