Julin S (Jan 11 2022 at 06:54): 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?
Théo Winterhalter (Jan 11 2022 at 06:59):Have you tried parentheses around the right-hand side and before the point?
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?)?
Paolo Giarrusso (Jan 11 2022 at 18:37):The RHS isn't separate from the notation options
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.
Julin S (Jan 12 2022 at 04:20):Okay, I think I get it now. Thanks!
Notification Bot (Jan 12 2022 at 04:20):Julin S has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC