[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

equality on characters


I was wondering whether equality is decidable on strings and characters.
For instance, is the following derivable ?

th : THEOREM NOT ("a" = "b")

and if so, how ? GRIND does not work.
It seems to boil down to the question whether 
char(<ascii-number-of-a>) =
char(<ascii-number-of-b>) is decidable. And since char is defined as a
constructor in a data-type, there is no reason why char(2) could not be
equal to char(3).

It seems to me that characters would be much more useful if equality was
decidable. I'm afraid that I will have to use integers instead because 
I need the decidability in my setting.

If there is a good reason for not assuming the inequality of, say,
"a" and "b", then I would like to know it.

Kind regards,


Indra Polak