The Coq mailing list

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

Dear all,

thank you very much for your replies and your time.

Yves Bertot wrote:
> Long answer:
>
> ...
> ...
> ...
>
> I hope this helps,
>
> Yves
Yes, it really helped my understanding (I hope ) in this topic. Thanks 
for the long answer in specific, it was quite informative.

However, I would like to rephrase, in a way, my question. I knew about 
the option of creating a string_dec function of type forall x y: string, 
{x=y}+{x<>y}, as in Yves' Semantics Survey. I'm concerned about the 
*evaluation* of the clause as well. For example the following:

Coq < Eval compute in (if (string_dec x y) then true else false).

to give me false as an answer, whereas the

Coq < Eval compute in (if (string_dec x x) then true else false).

to give me true. However, in that way I don't get this result.

Apologize for not setting it down properly in my first email, but my aim 
is to be able to do that kind of evaluations/computations, in order to 
get a *terminal* result from the evaluation.

Thank you very much in advance again,
Theo.

--
| 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"              |
--