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?

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

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?)?

The RHS isn't separate from the notation options

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`

.

Okay, I think I get it now. Thanks!

Julin S has marked this topic as resolved.

Last updated: Jun 15 2024 at 05:01 UTC