AgdaのMixfix演算子の空白の必要条件を取得しますか？

Question

Agdaに特定の文字が新しいトークンの先頭を示すことを伝える方法はありますか？例えば、私は（空想ユニコードブラケットで）次き：

私は

f （ e⃗ ） 

として使用しかし、私が本当に欲しいこと

f（e⃗） 

としてそれを使用することですができ

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

これを行うと、Agdaはそれが単一の識別子だと考え、範囲外のエラーを出します。これを回避する方法はありますか？

Answer 1

Agdaは、任意の連続する英数字および演算子文字を単一の識別子として解析します。 Agdaレクサーを変更しないと、この問題を回避する方法はありません。これはすべて名前が解決される前に起こります。そのため、特定の名前にスペースが必要ないことを宣言する方法はありません。

コードをもっとコンパクトに見せるために、他のユニコードの空白文字を使用してみることもできますが、うまく動作しているとは限りません。ゼロ幅のスペースは実際にはスペース文字ではなく、他のスペースは' 'と同じになります。