CODEWITHSUNDEEP
parsingoperatorsagdainfix-operator
Joey Eremondi
Joey Eremondi

Reputation: 8433

Get around whitespace requirement for Mixfix operators in Agda?

Is there a way to tell Agda that a certain character marks the beginning of a new token? For example, I have the following (with fancy unicode brackets):

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

which I can use as

f （ e⃗ ）

But what I'd really like is to use it as 

f（e⃗）

If I do that, Agda thinks that it's a single identifier, and gives a not-in-scope error. Is there a way around this?

Upvotes: 1

Views: 242

Answers (1)

Twan van Laarhoven
Twan van Laarhoven

Reputation: 2602

Agda parses any sequence of consecutive alphanumeric and operator characters as a single identifier. There is no way around this without changing the Agda lexer. This all happens way before names are resolved, so there would be no way to declare that spaces are not needed for certain names.

You could try using other unicode space characters to make your code look more compact, but I haven't found any that work well. Zero width spaces are apparently not actually a space character, and emacs renders other spaces the same as ' '.

Upvotes: 3

Related Questions