Autocompletion doesn't work with names containing operators, and case split doesn't work with names with one special character mixed with more characters or names with 3 or more characters

[ShreckYe]

Agda supports special characters including Unicode characters in names except for reserved ones, and sometimes it's a convention to write names with such characters. Currently autocompletion and case split don't work with such names.

[banacorn]

Thanks for reporting this. Can you give us one example for autocompletion and one for case splitting?

[ShreckYe]

See the code:

open import Data.Nat

≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans m≤n n≤p = {!   !}

<-trans : ∀ {m n p : ℕ} → m < n → n < p → m < p
<-trans m<n n<p = {!   !}

If I case split m≤n or m<n in the 2 holes, it reports errors:

Unbound variable m≤ when checking that the expression ? has type m ≤ p

Unbound variable m< when checking that the expression ? has type m < p

Autocompletion works for m≤n but not for m<n in the holes. I guess it's because VS Code treats < as an operator instead of part of the name, while ≤ is not treated as an operator.

[ShreckYe]

I tried some more code and it seems it's more than that: case split also doesn't work with variable names with 3 or more characters.

See the code:

open import Data.Nat

≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans abc n≤p = {!   !}

Case split doens't work with the name abc and it reports:

Unbound variable ab when checking that the expression ? has type m ≤ p

If I change the name to a or ab, it works.

So I then tested names containing special characters with less than 3 characters. See the form below:

Variable name	Does case split work?	Ubound variable reported in error
≤	yes
<	yes
m≤	not as expected: it splits the implicit argument m
m<	not as expected: it splits the implicit argument m
a≤	no	a
a<	no	a
≤n	no	≤
<n	no	<
≤≤	no	≤
<<	no	<
≤<	no	≤
<≤	no	<

So it seems I have made a mistake. The problem here is not just special characters, it's either names with one special character mixed with more characters or names with 3 or more characters.

[banacorn]

Autocompletion failed because VS Code doesn't know what constitutes a valid token in Agda.

You can also double click on names, and VS Code would select a group of characters that it considers to be a token. (m≤n would get selected as a whole, while m<n break into parts)

We can fix this by telling VS Code what constitutes a token, and we have already have the information in hand (from highlighting)!