Stream: math-comp users

Topic: ✔ negPf


view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 28 2023 at 06:53):

Pierre Jouvelot has marked this topic as resolved.

view this post on Zulip 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 of negPf (and others, if there are) in https://coq.inria.fr/library/Coq.ssr.ssrbool.html would have been nice.

Feel free to open a PR to add it.

view this post on Zulip Pierre Jouvelot (Aug 29 2023 at 13:43):

Pierre Jouvelot said:

Pierre Roux Will do then, with pleasure :)

Done.

view this post on Zulip Notification Bot (Aug 29 2023 at 13:44):

Pierre Jouvelot has marked this topic as resolved.


Last updated: Jul 15 2024 at 19:01 UTC