Kenji Maillard (Feb 19 2021 at 16:20): Kenji Maillard (Feb 19 2021 at 16:20):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 ?
Kenji Maillard (Feb 19 2021 at 16:23):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...).
Gaëtan Gilbert (Feb 19 2021 at 16:32):it gets printed fine (though not with 5, I guess because numeral notations interfere)
Kenji Maillard (Feb 19 2021 at 16:42):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..
Enrico Tassi (Feb 19 2021 at 17:28):it's a feature: https://github.com/coq/coq/blob/a2938972537389b9813794147412f51494f48dd1/theories/ssr/ssreflect.v#L213
Guillaume Melquiond (Feb 19 2021 at 17:33):That said, maybe all of those should be marked (only printing) to make them less confusing.
Li-yao (Feb 19 2021 at 17:40):What does that feature do actually?
Enrico Tassi (Feb 19 2021 at 17:44):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)
Enrico Tassi (Feb 19 2021 at 17:46):SSR => [: 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.
Kenji Maillard (Feb 19 2021 at 17:56):Thanks for the enlightning explanation @Enrico Tassi, I see how that can be useful as a print-only notation.
Enrico Tassi (Feb 19 2021 at 17:57):They are all "little hacks", I just warned in case you tried to remove that "feature"
Gaëtan Gilbert (Feb 19 2021 at 17:58):what's the "dummy" in odd-order for though? https://github.com/math-comp/odd-order/blob/19eb998e2d08c21c6e61806cc7b588238629757e/theories/PFsection3.v#L208
Enrico Tassi (Feb 19 2021 at 18:05):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).
Enrico Tassi (Feb 19 2021 at 18:07):And git is not helping: https://github.com/math-comp/mathcomp-history-before-github/commit/ca72e8eb87a1a7feb33c6d447dc2aa7e63940700
Last updated: Oct 04 2023 at 22:01 UTC