The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

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₃.

I'm sure there's more, but these are the ones I've currently bumped into.

Funnily, 

  Definition test : nat -> nat := fun 〈 => 〈.

doesn't work, but

  Notation "'〈' x = w , e ':' t '〉'" := (Epack w (fun x => t) e).

works; not sure if it's because 〈 is classified as some special punctuation
token or something.  All this was tested on Coq v 8.0pl1 at least.


        Stefan