The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

As far as I know, coq does not support the \uXXXX escape sequences,
but CoqIDE allows to input them directly : type CONTROL+SHIFT+211A and
you will see a marvellous bold math Q (if the font supports it...)

Hope this helps.
 
>>>>> "roconnor" == roconnor  
>>>>>Â <roconnor AT theorem.ca>
>>>>>  writes:

    roconnor> I want to define the notation
    roconnor> Notation " '\u211A\u207A' " := Qpositive.

    roconnor> but whenever I use it, coqide chokes at the \u207A with 
``Syntax error:
    roconnor> undefined token.  Why can I not use single quotes to make 2 or 
more
    roconnor> unicode characters into one token?

    roconnor> -- 
    roconnor> Russell O'Connor                                      
<http://r6.ca/>
    roconnor> ``All talk about `theft,''' the general counsel of the American 
Graphophone
    roconnor> Company wrote, ``is the merest claptrap, for there exists no 
property in
    roconnor> ideas musical, literary or artistic, except as defined by 
statute.''
    roconnor> --------------------------------------------------------
    roconnor> Bug reports: http://coq.inria.fr/bin/coq-bugs
    roconnor> Archives: http://pauillac.inria.fr/pipermail/coq-club
    roconnor>           http://pauillac.inria.fr/bin/wilma/coq-club
    roconnor> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |