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:
As a result of those three points, I know how to build the notation for, say:
⟪
■ □ □ ⏎
□ ■ □ ⏎
□ □ ■ ⏎
⟫
But can I do better?
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)
*)
not sure if it's possible to get rid of only printing
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
.
I don't think it's possible to get the lexer to differentiate between
■□□
□■□
□□■
and
■□□□■□□□■
with notations
(assuming 1 box = 1 token)
make the end-of-line marker a zero-width space
Last updated: Oct 13 2024 at 01:02 UTC