Hello, when editing a .lagda.org file in agda2-mode in emacs, I find the following bug:
If between two code blocks, there is a {-1} thing (for instance, in some latex inline math), then the hole in a code block after the {-1} is not detected. However, if I put a space between the minus sign (like { -1} it is fine.
The second hole is not expanded:
# file.lagda.org
#+begin_src agda2
y = {!!}
#+end_src
{-1}
#+begin_src agda2
x = {!!}
#+end_src
The second hole is expanded:
# file.lagda.org
#+begin_src agda2
y = {!!}
#+end_src
{ -1}
#+begin_src agda2
x = {!!}
#+end_src
Agda version 2.7.0.1
GNU Emacs 30.0.92 (build 1, x86_64-pc-linux-gnu, GTK+ Version 3.24.43, cairo version 1.18.2)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4