Stream: Coq users

Topic: ✔ /\\ typo or real syntax?


view this post on Zulip Anders Larsson (Oct 27 2022 at 18:55):

Arre the /\\ and \\/ operators real or just a typo?

image.png

From:
https://coq.inria.fr/distrib/current/refman/addendum/micromega.html#coq:flag.Nra-Cache

But here the operators looks normal:
https://coq.github.io/doc/V8.11.0/refman/addendum/micromega.html#coq:flag.nra-cache

view this post on Zulip Gaëtan Gilbert (Oct 27 2022 at 21:00):

they're not real

view this post on Zulip Notification Bot (Oct 27 2022 at 21:14):

Anders Larsson has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Oct 28 2022 at 15:03):

Probably an artifact from LaTeX

view this post on Zulip Jason Gross (Nov 01 2022 at 01:04):

I've reported this at https://github.com/coq/coq/issues/16761


Last updated: Apr 19 2024 at 00:02 UTC