When I tried to copy some code from the book, I faced some messages like “syntax error: lexer: undefined token”.
I realized the problem which is the ⇒ is not the same as => in code.
I guess you are copying the code from the online page: FYI, if you download the book instead, the source code is in ascii.
That said, those notations are defined in the standard library, so, at least as for CoqIDE, you just need a specific import to enable them:
Require Import Unicode.Utf8.
Check (∀ x, x = 0).
You can find more info here:
https://coq.inria.fr/refman/practical-tools/coqide.html#using-unicode-symbols
1 Like
Yes, you are right ! Thank you advice.
Now I use emacs as my editor, everything is ok for me.