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

**URL:** <https://discourse.rocq-prover.org/t/about-syntax-error-lexer-undefined-token-at-the-beginning/2081>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [October 19, 2023, 5:16am UTC](https://discourse.rocq-prover.org/t/about-syntax-error-lexer-undefined-token-at-the-beginning/2081 "2023-10-19T05:16:04Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![tomlogo](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tomlogo/32/887_2.png) [@tomlogo](https://discourse.rocq-prover.org/u/tomlogo)\
**Post date:** [October 19, 2023, 5:16am UTC](https://discourse.rocq-prover.org/t/about-syntax-error-lexer-undefined-token-at-the-beginning/2081/1 "2023-10-19T05:16:04Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [October 20, 2023, 12:52pm UTC](https://discourse.rocq-prover.org/t/about-syntax-error-lexer-undefined-token-at-the-beginning/2081/2 "2023-10-20T12:52:47Z")

</div>

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:

```auto
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](https://coq.inria.fr/refman/practical-tools/coqide.html#using-unicode-symbols)

---

<div class="post-metadata">

**Author:** ![tomlogo](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tomlogo/32/887_2.png) [@tomlogo](https://discourse.rocq-prover.org/u/tomlogo)\
**Post date:** [October 20, 2023, 10:28pm UTC](https://discourse.rocq-prover.org/t/about-syntax-error-lexer-undefined-token-at-the-beginning/2081/3 "2023-10-20T22:28:43Z")

</div>

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