Pierre Jouvelot (Aug 28 2023 at 06:32): Pierre Jouvelot (Aug 28 2023 at 06:32):Thanks a lot @Paolo Giarrusso: I wouldn't have thought of this type of behavior, which runs contrary to at least my intuitive understanding of reflection here.
I think that a side comment, say (* Warning: doesn't operate both ways as usual (see ....). *), beside the documentation of negPf (and others, if there are) in https://coq.inria.fr/library/Coq.ssr.ssrbool.html would have been nice.
Notification Bot (Aug 28 2023 at 06:53):Pierre Jouvelot has marked this topic as resolved.
Pierre Roux (Aug 28 2023 at 07:29):Pierre Jouvelot said:
I think that a side comment, say
(* Warning: doesn't operate both ways as usual (see ....). *), beside the documentation ofnegPf(and others, if there are) inhttps://coq.inria.fr/library/Coq.ssr.ssrbool.htmlwould have been nice.
Feel free to open a PR to add it.
Pierre Jouvelot (Aug 29 2023 at 13:43):Pierre Jouvelot said:
Pierre Roux Will do then, with pleasure :)
Done.
Notification Bot (Aug 29 2023 at 13:44):Pierre Jouvelot has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC