Stream: Hierarchy Builder devs & users

Topic: Variable naming error


view this post on Zulip Karl Palmskog (Oct 14 2023 at 07:19):

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]). *)

view this post on Zulip Paolo Giarrusso (Oct 14 2023 at 07:23):

Is v1 a keyword?

view this post on Zulip Karl Palmskog (Oct 14 2023 at 07:30):

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

view this post on Zulip Karl Palmskog (Oct 14 2023 at 08:00):

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.

view this post on Zulip Enrico Tassi (Oct 14 2023 at 19:08):

Oops https://github.com/math-comp/hierarchy-builder/blob/2a109287597862e40361531a33154eabb7749cb6/structures.v#L1056

view this post on Zulip Karl Palmskog (Oct 14 2023 at 19:11):

ah, should be easy to fix?

view this post on Zulip Enrico Tassi (Oct 14 2023 at 19:12):

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

view this post on Zulip Karl Palmskog (Oct 14 2023 at 19:13):

isn't Notation "[find v1 , .., vn | t1 ∼ t2 ] rest" := enough? (a space after the v1)

view this post on Zulip Enrico Tassi (Oct 14 2023 at 19:36):

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

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:44):

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.

Identifiers enclosed in single quotes are treated as symbols and thus lose their role as parameters.

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:44):

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

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:46):

Ah also

The notation consists of tokens separated by spaces.

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 01:48):

So quotes are only needed to turn identifiers into keywords


Last updated: Apr 21 2024 at 02:41 UTC