Stream: Coq users

Topic: ✔ Error while creating simple notation


view this post on Zulip Julin S (Jan 11 2022 at 06:54):

I was trying to make << as sort of a short-form for Nat.ltb and tried

Notation "x << y" := Nat.ltb x y.

but got an error at the point of the last x as:

Syntax error: '.' expected after [vernac:syntax_command] (in [vernac_aux]).

Why is this happening?

view this post on Zulip Théo Winterhalter (Jan 11 2022 at 06:59):

Have you tried parentheses around the right-hand side and before the point?

view this post on Zulip Julin S (Jan 11 2022 at 07:02):

That worked! Thanks. Why is the parenthesis needed though? I mean the part that comes after := is clearly separate when coq looks at it, right (gallina term?)?

view this post on Zulip Paolo Giarrusso (Jan 11 2022 at 18:37):

The RHS isn't separate from the notation options

view this post on Zulip Paolo Giarrusso (Jan 11 2022 at 18:38):

if you take Notation "●{ dq } a" := (auth_auth dq a) (at level 20, format "●{ dq } a"). (random notation from some Coq code) and drop the parens, you get Notation "●{ dq } a" := auth_auth dq a (at level 20, format "●{ dq } a"). where at level ... could be an argument of auth_auth.

view this post on Zulip Julin S (Jan 12 2022 at 04:20):

Okay, I think I get it now. Thanks!

view this post on Zulip Notification Bot (Jan 12 2022 at 04:20):

Julin S has marked this topic as resolved.


Last updated: Jan 29 2023 at 05:03 UTC