Stream: Coq users

Topic: Breaking notation strings across multiple lines

Lennard Gäher (Mar 18 2021 at 12:41):

Hi everyone,
I am trying to set up some notations with format strings which can get quite large. To increase readability of the format strings, I'd like to split them across multiple lines. Is there a way to do that?
I've attempted to do it by writing multiple string literals on subsequent lines (as one could do in C-like languages), e.g.

Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
  ([(k1, a1); (k2, a2)])
  (at level 1, format
  "{[ '[    ' k1  :=  a1 ; ']' "
   " '/  ' '[    ' k2  :=  a2 ']' "
   "]}").

but that does not seem to work.

Enrico Tassi (Mar 18 2021 at 12:50):

I don't think it is possible. One suggestion I could give you is to separate the command into two, Reserved Notation and Notation which will make the lines shorter.

Last updated: Apr 20 2024 at 07:01 UTC