Agda on windows: `→ ` not in scope

Question

I'm trying to run chapter 1 of Programming Language Foundations in Agda on a Windows machine.

This is a fresh install of Agda 2.5.2 and Emacs 25.1.1 from the MSI and untouched Agda code from the textbook.

I'm getting this error:

Not in scope:
  → at C:\bb\plfa.github.io\src\plfa\Naturals.lagda:51,14-17
when scope checking →

When I run agda on the command line, I get a similar error message, this time with the → character rendered correctly:

Checking plfa.Naturals (C:\bb\plfa.github.io\src\plfa\Naturals.lagda).
C:\bb\plfa.github.io\src\plfa\Naturals.lagda:51,14-17
Not in scope:
  → at C:\bb\plfa.github.io\src\plfa\Naturals.lagda:51,14-17
when scope checking →

The line Agda is complaining about is the last one in this code block:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
\end{code}

The same code runs fine on Ubuntu.

I confirmed that the character is correct: I get the same result if I delete it and type \to.

Answer 1

Do you have similar problems compiling other files that aren't PLFA-related? This sounds a lot more like an Agda issue than a PLFA issue. If it isn't I can recommend trying Agda 2.5.4.2, which is the current minimal version for PLFA (see https://plfa.github.io/GettingStarted/)