2

(Hello, thanks in advance) I'm working through the introduction to HoTT in agda https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html

and Started my own Agda project (2 files, hardly a project) as I work through the lecture notes, However Load(ing) my file from Atom's agda-mode menu I get this error

agda:14,19: Lexical error (unprintable character): ℓ

I went back and loaded the agda file in the lecture notes' git project and it typechecks fine. I've gone so far as to replace the offending line of code with the same line from the original complete (and typechecking) file and still get the same error

Maybe this is easy solve/stupid question hoping I can get some help

gallais
  • 11,823
  • 2
  • 30
  • 63
Mzk Levi
  • 814
  • 7
  • 14
  • 1
    You'd get more help, if you posted the problematic file, because otherwise it's really hard to guess what might went wrong. – effectfully Nov 26 '19 at 11:22
  • 2
    If I had to guess, I'd say it is something to do with your Atom configuration. Anf you didn't put an Atom tag on your question. – Jacques Carette Nov 26 '19 at 12:47
  • I get that error quite a bit, have you tried writing the line out without copying and pasting? – oisdk Nov 26 '19 at 22:27
  • yes I had typed it out originally, I ended up copying and pasting to test the extent of the error – Mzk Levi Nov 27 '19 at 00:57

0 Answers0