Stream: math-comp analysis

Topic: question about the notation for image


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

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

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

view this post on Zulip Reynald Affeldt (Sep 17 2021 at 14:46):

Thank you! I put an entry in the FAQ for me to remember. ^_^


Last updated: Aug 19 2022 at 19:03 UTC