The Coq mailing list

[Fr�d�ric Besson <fbesson AT irisa.fr>]

On 16 janv. 08, at 20:18, Theodoros G. Tsokos wrote:

> Dear all,
>
> I'm having the following definition (representing identifiers of a  
> language)
>
> Variable string : Type.
> Variables x y z : string.
Do you really want to keep the string type abstract ?

If no, you can use the Coq string library - there is a string_dec  
function
Require Import String
Variables x y z : string

If yes, you will have to axiomatize further and make the hypothesis  
of a string comparison function
Variable compare_string : string -> string -> bool.
Variable compare_string_correct : ....


Regards,

--
Frédéric Besson
>