The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

Here is a quick reply to your Dec 20 mail.

> The following uses of Unicode (using utf-8 encoding) don't work:
> 
>   Definition test : nat -> nat := fun Θ => Θ.
>   Definition test : nat -> nat := fun Δ => Δ.
>   Definition test : nat -> nat := fun Γ => Γ.
>   Definition test : nat -> nat := fun τ => τ.
>   Definition test : nat -> nat := fun φ => φ.
>   Definition test : nat -> nat := fun ○ => ○.
>   Definition test : nat -> nat := fun ▹ => ▹.
>   Definition test : nat -> nat := fun ▷ => ▷.
>   Definition test : nat -> nat := fun x₁ => x₁.
>   Definition test : nat -> nat := fun x₂ => x₂.
>   Definition test : nat -> nat := fun x₃ => x₃.

Only a few Unicode ranges are indeed supported in Coq. The reason is
that Coq makes a distinction between letters (or more generally
components of identifiers) and symbols and that this requires a
detailed analysis of what is in each Unicode range (e.g. in the range
for Latin-1 - not yet supported in Coq -, two symbols are hidden -
× and ÷ - in the middle of a full range of letters).

In V8.0 (new syntax), only the ranges for Greek letter, letter-like
symbols (e.g. ℤ) and various mathematical symbols are supported.

Especially, your first four examples actually work. The next three
examples cannot work because the Unicode elements that you use are not
letters, hence not acceptable as valid identifiers (and in practice
these elements are not supported at all in V8.0, even as symbols).
The last three examples could be supported and they will in the next
release of Coq.

> Funnily, 
> 
>   Definition test : nat -> nat := fun 〈 => 〈.
> 
> doesn't work, but
> 
>   Notation "'〈' x = w , e ':' t '〉'" := (Epack w (fun x => t) e).
> 
> works.

The Unicode elements 〈 and 〉 are indeed supported in V8.0. For the
reason that there are considered as symbols in Coq, the first case
correctly fails and the second works. As a side remark, precisely
because they are symbols, you don't need to surround them by quotes in
the notation.

Hugo Herbelin