agda-mode

agda-mode copied to clipboard

Whenever I undo while agda-mode is active, it undoes twice. This is rather inconvenient! This is on a fresh install of Atom and agda-mode from December 2; Atom 1.53.0, agda-mode...

elidupree

Bumps [ini](https://github.com/isaacs/ini) from 1.3.5 to 1.3.7. Commits c74c8af 1.3.7 024b8b5 update deps, add linting 032fbaf Use Object.create(null) to avoid default object property hazards 2da9039 1.3.6 cfea636 better git push script,...

dependabot[bot]

It would be great to be able to use Atom in order to work with `.lagda.md` source files. Would it be difficult to extend `agda-mode` to work with this different...

lclem

Bumps [elliptic](https://github.com/indutny/elliptic) from 6.4.1 to 6.5.3. Commits 8647803 6.5.3 856fe4d signature: prevent malleability and overflows 6048941 6.5.2 9984964 package: bump dependencies ec735ed utils: leak less information in getNAF() 71e4e8e 6.5.1...

dependabot[bot]

Bumps [lodash](https://github.com/lodash/lodash) from 4.17.15 to 4.17.19. Release notes Sourced from lodash's releases. 4.17.16 Commits d7fbc52 Bump to v4.17.19 2e1c0f2 Add npm-package 1b6c282 Bump to v4.17.18 a370ac8 Bump to v4.17.17 1144918...

dependabot[bot]

QuickLaTeX backend howto?

5

Hi, is it possible from the Atom's agda-mode to access the [QuickLaTeX backend](https://agda.readthedocs.io/en/latest/tools/generating-latex.html?highlight=quicklatex#quicker-generation-without-typechecking) to load a scope-checked version of the code?

pnlph

Interacting within agda code in Atom

3

Hi, i am searching for an Atom package that allows to interact better with language services like go-to-definition. I found the [atom-ide-ui](https://atom.io/packages/atom-ide-ui) package, but language integrations should be built on...

pnlph

Go to definition for mixfix operators without underscore fails

1

Related with #119 and #122. I noticed that when I try to get the `Scope Info` of the constructor `_,_`, the `agda-mode` replies that `, is not in scope.` Example:...

pnlph

As titled, here's a minimal file for reproducing it: ```agda a = (?) ```

banacorn

Scope info does not provide links for the openings

4

When calling the `go-to-definition` command i am getting the links to the definitions but not to the openings, but it seems that the link should be there because of the...

pnlph