CODEWITHSUNDEEP
unicodecoqproof-general
user1868607
user1868607

Reputation: 2610

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?

Upvotes: 3

Views: 1325

Answers (1)

Ptival
Ptival

Reputation: 9447

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.

Upvotes: 2

Related Questions