有没有办法告诉agda某个字符标志着新令牌的开始？例如，我有以下内容（带有花哨的Unicode括号）：
data Term where
_（_） : Term -> Term -> Term
我可以用作
f （ e⃗ ）
但是我真正想要的是用作
f（e⃗）
如果我这样做，Agda认为它是一个单个标识符，并且会出现不中的错误。有办法解决吗？
AGDA作为单个标识符来解析任何连续字母数字和操作符字符的任何序列。没有更改Agda Lexer，就无法解决。在解决名称之前，这一切都发生了，因此无法声明某些名称不需要空间。
您可以尝试使用其他Unicode太空字符来使您的代码看起来更紧凑，但是我没有发现任何效果很好。零宽度空间显然不是一个空间特征，而Emacs则与' '相同的其他空间。