parsing - 绕过 Agda 中 Mixfix 运算符的空白要求？

Question

有没有办法告诉 Agda 某个字符标志着一个新令牌的开始？例如，我有以下（带有花哨的 unicode 括号）：

data Term where
  _（_） : Term -> Term -> Term

我可以用作

f （ e⃗ ）

但我真正想要的是将它用作

f（e⃗）

如果我这样做，Agda 会认为它是一个标识符，并给出一个不在范围内的错误。有没有解决的办法？

Answer 1

Agda 将任何连续的字母数字和运算符字符序列解析为单个标识符。如果不更改 Agda 词法分析器，就无法解决这个问题。这一切都发生在解析名称之前，因此无法声明某些名称不需要空格。

您可以尝试使用其他 unicode 空格字符来使您的代码看起来更紧凑，但我没有发现任何效果很好。零宽度空格显然不是真正的空格字符，并且 emacs 将其他空格呈现为' '.