The Coq mailing list

["Theodoros G. Tsokos" <T.Tsokos AT cs.bham.ac.uk>]

Dear all,

I'm having the following definition (representing identifiers of a language)

Variable string : Type.
Variables x y z : string.

I'm trying to find a way to compare the above strings, that is the 
identifiers themselves, not their values, and get a boolean number as an 
output. That is, something like:

Variables A B : string.
if (A=B) then true else false.

where :
for A= x and B=x it'll give me true, but for A=x and B=y it'll give me 
false.

I tried to use sumbool, like implemented in Yves Bertot's Semantics 
Survey [1] :
Variable string_dec : forall a b:string, {a=b}+{a<>b}

but I got really confused.

Thank you very much in advance for your time and help. It's probably a 
trivial solution so apologize for using the list for something like that.

Regards,
Theo.

[1] http://coq.inria.fr/contribs/Semantics_survey.html

--
| Theodoros G. Tsokos                                      |
| http://www.cs.bham.ac.uk/~txt                            ;|
| School of Computer Science, The University of Birmingham |
| Edgbaston, Birmingham, B15 2TT, United Kingdom           |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "The freedom of speech includes the freedom to shut up"  |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "Democracy: the freedom to say whatever one wants and    |
| the capital to implement whatever it wants"              |
--