I just found out that Coq accepts notations containing comments delimiters without complaining, and then fail to make sense out of the resulting mess:
Notation "(*ghost*)" := (5). (* Accepting readily *) Check (*ghost*). (* Error: *) (* Syntax error: [constr:lconstr] expected after 'Check' (in [vernac:query_command]). *) Definition x := (*ghost*). (* Error: Syntax error: [reduce] expected after ':=' (in [vernac:def_body]). *)
Is that a bug or a feature ?
The context is that I'm trying to make sense of this line of Coq code, but that's probably a no-op (up to side effects...).
it gets printed fine (though not with
5, I guess because numeral notations interfere)
So that would be a way not to print some garbage term ?
I still don't understand how that can be usefull in the example I linked because the rhs does not seem to typecheck..
it's a feature: https://github.com/coq/coq/blob/a2938972537389b9813794147412f51494f48dd1/theories/ssr/ssreflect.v#L213
That said, maybe all of those should be marked
(only printing) to make them less confusing.
What does that feature do actually?
Another use case https://github.com/coq/coq/blob/a2938972537389b9813794147412f51494f48dd1/theories/ssr/ssreflect.v#L80-L86 which requires it to be a parsing one (but which cannot be actually parsed)
=> [: H ] and
abstract: H manage a proof variable
H whose type is initially an evar and later a a term. When it is an evar, we print a number, when it gets assigned we print the number in comment. But if you copy paste the type, the number does not get in the way, since it is commented. I think we could survive without that number being printed... but being able to print it in a comment seems a feature to me.
Thanks for the enlightning explanation @Enrico Tassi, I see how that can be useful as a print-only notation.
They are all "little hacks", I just warned in case you tried to remove that "feature"
what's the "dummy" in odd-order for though? https://github.com/math-comp/odd-order/blob/19eb998e2d08c21c6e61806cc7b588238629757e/theories/PFsection3.v#L208
It's funny because I don't know, even if
Prop Prop is a term I like to use when I want o assert it does not occur (e.g. as an unused argument of a notation).
And git is not helping: https://github.com/math-comp/mathcomp-history-before-github/commit/ca72e8eb87a1a7feb33c6d447dc2aa7e63940700
Last updated: Feb 09 2023 at 00:03 UTC