Quinn (Oct 20 2021 at 04:53): Quinn (Oct 20 2021 at 04:53):I'm often confused at Notation declarations.
Inductive term : Type :=
...
| LLNeg : term -> term
...
.
Notation "C '^False'" := LLNeg C.
Fails with Error: Syntax error: '.' expected after [vernac:syntax_command] (in [vernac_aux])..
Intuitively I'm not quantifying or binding in any way C, so I get why maybe it's not gonna work. But I read a lot of code examples where this basically does work! and it works _sometimes_ for me just not this evening.
Paolo Giarrusso (Oct 20 2021 at 07:54):I think you want Notation … := (LLNeg C). not := LLNeg C., those parentheses are _not_ redundant
Paolo Giarrusso (Oct 20 2021 at 07:54):that’s because you can write := (the expansion) (some information about the notation).
Paolo Giarrusso (Oct 20 2021 at 07:58):The Coq error message is very far from great, but it does say “Syntax error”, and the syntax analysis (parsing) comes before names are analysed (OTOH, notation scopes must be dealt after)
Paolo Giarrusso (Oct 20 2021 at 07:58):and the way you bind Cis perfectly fine :-)
Quinn (Oct 20 2021 at 16:11):ok fantastic, thanks!
Notification Bot (Oct 20 2021 at 16:11):Quinn has marked this topic as resolved.
Last updated: Oct 04 2023 at 23:01 UTC