About 'syntax error: lexer: undefined token' at the beginning

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:

1 Like

Yes, you are right ! Thank you advice.
Now I use emacs as my editor, everything is ok for me.