unicodecoqproof-general

Unicode symbols fail for Proof-general while writing Coq

I use Coq 8.11 in Ubuntu with Proof-general. I write:

Ltac example1 := fail.

and succeed. Say I want to use unicode symbols:

Proof-General -> Display -> Quick Options -> Unicode Tokens

then I write again:

Ltac example2 ≔ fail.

and fail with the error:

Error: Syntax Error: Lexer: Undefined token

So I go to some editor and write the sequence ":=" and copy paste it while writing:

Ltac example3 := fail.

Happily I succeed again.

The above occurs with many symbols you can think of |-, /\, /, etc.

How can i solve it?

Solution

  • So, there is a difference between displaying Unicode tokens, and recognizing Unicode tokens as input.

    Displaying Unicode tokens works as a sort of visual ligature, while the underlying text remains ASCII. It means, you type :=, and the editor displays ≔, but if you open with another editor, you will still see :=.

    Now if you want to use Unicode tokens in your code, you can, but you need to let the Coq process know that you are doing so, by importing the Unicode.Utf8 module:

    From Coq Require Import Unicode.Utf8.