Agda의 Mixfix 운영자를위한 공백 요구 사항을 알아 보시겠습니까?

Question

Agda에게 특정 문자가 새 토큰의 시작을 표시한다고 말할 수있는 방법이 있습니까?

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

내가

f （ e⃗ ） 

로 사용하지만 내가 좋아하는 정말 줄 것은

f（e⃗） 

로 사용하는 것입니다 수 있습니다 : 예를 들어, 나는 (공상 유니 코드 브래킷) 다음이

내가 그렇게하면 Agda는 이것이 단일 식별자라고 생각하고 범위 오류를 제공하지 않습니다. 이 문제를 해결할 방법이 있습니까?

Answer 1

Agda는 연속되는 영숫자 및 연산자 문자의 시퀀스를 단일 식별자로 구문 분석합니다. Agda 렉서를 변경하지 않고이 문제를 해결할 방법은 없습니다. 이름이 해석되기 전에 모든 일이 발생하므로 특정 이름에 공백이 필요 없다는 것을 선언 할 방법이 없습니다.

다른 유니 코드 공간 문자를 사용하여 코드를 좀 더 작게 보이도록 시도 할 수는 있지만 제대로 작동하지 않습니다. 너비가 0 인 공백은 실제로 공백 문자가 아니며 emacs는 다른 공백을 ' '과 동일하게 렌더링합니다.