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