Stream: Coq users

Topic: How little spacing/delimit can I get away with in notations?


view this post on Zulip Valentin Robert (Feb 29 2024 at 18:02):

I've been wanting to essentially have this notation:

■□□
□■□
□□■

standing for something along the lines of:

[ [true; false; false]
; [false; true; false]
; [false; false; true]
]

Now, my gut feeling is I won't be able to get away with it for multiple reasons, but I would like to ascertain exactly how little help I need to sprinkle to keep the notation as concise as possible.

What I see as potential problems:

  1. the lack of spacing between characters
  2. the lack of begin/end markers
  3. the lack of end-of-line markers

As a result of those three points, I know how to build the notation for, say:


   
   
   

But can I do better?

view this post on Zulip Gaëtan Gilbert (Feb 29 2024 at 18:15):

Module ListNotations.
Notation "[ ]" := nil (format "[ ]") : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))
  (format "[ '[' x ;  '/' y ;  '/' .. ;  '/' z ']' ]") : list_scope.
End ListNotations.
Import ListNotations.
Open Scope list_scope.

Notation "" := (@nil _) (only printing).

Declare Custom Entry sublist.

Notation "x y" := (@cons (list bool) x y) (only printing, x custom sublist, format "x '//' y", at level 10, right associativity).


Notation "" := (@nil _) (only printing, in custom sublist).

Notation "x y" := (@cons bool x y) (only printing, in custom sublist at level 9, x constr, y custom sublist, format "x y", right associativity).

Notation "■" := true.
Notation "□" := false.

Check
[ [true; false; false]
; [false; true; false]
; [false; false; true]
]
.
(*
■□□
□■□
□□■

     : list (list bool)
*)

view this post on Zulip Gaëtan Gilbert (Feb 29 2024 at 18:15):

not sure if it's possible to get rid of only printing

view this post on Zulip Valentin Robert (Feb 29 2024 at 18:16):

Oh, I was being ambiguous, I actually cared more about it as an input notation. But this is nice too.
I'm now considering parsing the input from a string.

view this post on Zulip Gaëtan Gilbert (Feb 29 2024 at 18:18):

I don't think it's possible to get the lexer to differentiate between

■□□
□■□
□□■

and

■□□□■□□□■

with notations
(assuming 1 box = 1 token)

view this post on Zulip Li-yao (Mar 01 2024 at 08:41):

make the end-of-line marker a zero-width space


Last updated: Jun 13 2024 at 21:01 UTC