Stream: Coq users

Topic: ✔ Making a custom entry

Julin S (Jan 11 2022 at 10:37):

I was trying to make notations with custom entry like

Declare Custom Entry cename.

Notation "{{ e }}" := (e) (e custom cename at level 100).

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..)
  (in custom cename at level 50).

That ran without giving error. But when I try to use the notation, I get error:

Compute {{ [1;2] }}.
(*
Syntax error: [constr:cename] expected after '[' (in [constr:cename]).
*)

How can this be set right?

Gaëtan Gilbert (Jan 11 2022 at 10:41):

you need to also tell it x constr

Julin S (Jan 11 2022 at 10:47):

Thanks. Found this in here as well:

Rules associated with an entry can refer different sub-entries. The grammar entry name constr can be used to refer to the main grammar of term as in the rule

Does that also mean that y constr is also somehow inferred?

Notification Bot (Jan 11 2022 at 10:54):

Julin S has marked this topic as resolved.

Ali Caglayan (Jan 11 2022 at 15:02):

I don't know if it is inferred, but it doesn't hurt to be explicit about it.

Julin S (Jan 12 2022 at 10:16):

I modified this example to add a notation that takes a nat and 'implicitly' adds a '2' to it like:

Declare Custom Entry cename.

Notation "{{ e }}" := (e) (e custom cename at level 100).

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..)
  (in custom cename at level 50).

Notation "< x >" := (x + 2)
  (in custom cename at level 5, x constr).

but got error when using it:

Check {{ <2> }}.
(*
Syntax error: [constr:operconstr] expected after '>' (in [constr:operconstr]).
*)

How can this be fixed?

Julin S (Jan 12 2022 at 10:19):

Locate "< _ >". is giving:

Notation
"< x >" := Nat.add x (S (S O)) (default interpretation)

Does it being in default interpretation okay? Should it be displaying the name of the custom entry instead?

Li-yao (Jan 12 2022 at 14:21):

Notation "< x >" := (x + 2)
  (in custom cename at level 5, x constr at level 0).

Otherwise there's a conflict and the parser thinks > means the infix operator _ > _.

Julin S (Jan 12 2022 at 15:54):

Thanks!

Last updated: Oct 01 2023 at 18:01 UTC