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?
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.
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).
Thank you! I put an entry in the FAQ for me to remember. ^_^
Last updated: Feb 05 2023 at 06:28 UTC