Guillaume,

many thanks for your answer. But:

Le 9 mai 2014 à 16:22, Guillaume Melquiond <guillaume.melqui...@inria.fr> a 
écrit :

>> 2- is it fair to use Classical logic in the Coq stubs translated from Why3 
>> goals/lemmas ?
> 
> Yes, it is fair, since the logic of Why3 already assumes it.
> 
> In practice, I never had to assume it though, when doing a Coq proof. Indeed, 
> most of the predicates I get from Why3 are trivially boolean in nature, and 
> thus do not need excluded middle.

what do you mean by "most of the predicates I get from Why3 are trivially 
boolean in nature" ? In the Coq files that I get from Why3, I see Coq ‘Prop’s 
translated from Why3 predicates!!

-JJ-
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club

Reply via email to