Stream: Coq users

Topic: ✔ Notation arguments, quantifiers?


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

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 07:54):

I think you want Notation … := (LLNeg C). not := LLNeg C., those parentheses are _not_ redundant

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 07:54):

that’s because you can write := (the expansion) (some information about the notation).

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

view this post on Zulip Paolo Giarrusso (Oct 20 2021 at 07:58):

and the way you bind Cis perfectly fine :-)

view this post on Zulip Quinn (Oct 20 2021 at 16:11):

ok fantastic, thanks!

view this post on Zulip Notification Bot (Oct 20 2021 at 16:11):

Quinn has marked this topic as resolved.


Last updated: Feb 01 2023 at 11:04 UTC