Am I hitting some known bug in HB here? (Coq 8.18.0, MC 2.0.0, tried on both HB 1.5.0 and 1.6.0)

```
From HB Require Import structures. (* this is required for the error *)
From mathcomp Require Import all_ssreflect.
Definition fv A (l1 l2 : seq A) := exists2 v, v = l1 ++ l2 & true.
(* v works fine *)
Definition fv2 A (l1 l2 : seq A) := exists2 v2, v2 = l1 ++ l2 & true.
(* v2 works fine *)
Definition fv1 A (l1 l2 : seq A) := exists2 v1, v1 = l1 ++ l2 & true.
(* Error: Syntax error: ''' or [name] expected after 'exists2' (in [binder_constr]). *)
```

Is v1 a keyword?

that would explain it, but kind of nonsensical if HB introduces this keyword, it's probably used in lots of existing code

even more strange: if it's due to a keyword, it's `v1,`

rather than `v1`

, the following works:

```
Definition fv11 A (l1 l2 : seq A) := exists2 v1 , v1 = l1 ++ l2 & true.
```

ah, should be easy to fix?

I guess so, but I'm very bad at notations :-)

isn't `Notation "[find v1 , .., vn | t1 ∼ t2 ] rest" :=`

enough? (a space after the `v1`

)

I hope so, but I always thought one needs ' to introduce keywords, so I'm actually clueless

I also forget but the manual technically does explain it. Quoting with extra emphasis:

Tokens which are identifiers (such as A, x0', etc.) are the parameters of the notation. Each of them must occur at least once in the abbreviated term.

The other elements of the string (such as /\) are the symbols, which must appear literally when the notation is used.

Identifiersenclosed insingle quotesare treated as symbols and thus lose their role as parameters.

(from https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#basic-notations)

Ah also

The notation consists of tokens separated by spaces.

So quotes are only needed to turn identifiers into keywords

Last updated: Apr 21 2024 at 02:41 UTC