Reynald Affeldt (Sep 17 2021 at 13:27): Reynald Affeldt (Sep 17 2021 at 13:27):The image notation (the one with the @ and the backquote) keeps on printing as [set E | x in A]. Was this intended or is my setting wrong?
Pierre Roux (Sep 17 2021 at 13:55):It is defined as an only parsing notation https://github.com/math-comp/analysis/blob/master/theories/classical_sets.v#L291 so I guess this is expected.
Pierre Roux (Sep 17 2021 at 13:57):the printing notation being https://github.com/math-comp/analysis/blob/master/theories/classical_sets.v#L215 (I don't know how Coq would behave if both notations were available for printing).
Reynald Affeldt (Sep 17 2021 at 14:46):Thank you! I put an entry in the FAQ for me to remember. ^_^
Last updated: Feb 05 2023 at 06:28 UTC