whitespace-sensitive notation

Author: datokrat

src/Init/Data/Slice/Basic.lean

@@ -25,18 +25,18 @@ structure _root_.Std.Slice (shape : RangeShape) (α : Type u) {β : Type v}
   carrier : α
   range : PRange shape β
 
-syntax:max term "[" withoutPosition(term "...*") "]" : term
-syntax:max term "[" withoutPosition("*...*") "]" : term
-syntax:max term "[" withoutPosition(term "<...*") "]" : term
-syntax:max term "[" withoutPosition(term "...<" term) "]" : term
-syntax:max term "[" withoutPosition(term "<...<" term) "]" : term
-syntax:max term "[" withoutPosition("*...<" term) "]" : term
-syntax:max term "[" withoutPosition(term "...=" term) "]" : term
-syntax:max term "[" withoutPosition(term "<...=" term) "]" : term
-syntax:max term "[" withoutPosition("*...=" term) "]" : term
-syntax:max term "[" withoutPosition(term "..." term) "]" : term
-syntax:max term "[" withoutPosition(term "<..." term) "]" : term
-syntax:max term "[" withoutPosition("*..." term) "]" : term
+syntax:max term noWs "[" withoutPosition(term "...*") "]" : term
+syntax:max term noWs "[" withoutPosition("*...*") "]" : term
+syntax:max term noWs "[" withoutPosition(term "<...*") "]" : term
+syntax:max term noWs "[" withoutPosition(term "...<" term) "]" : term
+syntax:max term noWs "[" withoutPosition(term "<...<" term) "]" : term
+syntax:max term noWs "[" withoutPosition("*...<" term) "]" : term
+syntax:max term noWs "[" withoutPosition(term "...=" term) "]" : term
+syntax:max term noWs "[" withoutPosition(term "<...=" term) "]" : term
+syntax:max term noWs "[" withoutPosition("*...=" term) "]" : term
+syntax:max term noWs "[" withoutPosition(term "..." term) "]" : term
+syntax:max term noWs "[" withoutPosition(term "<..." term) "]" : term
+syntax:max term noWs "[" withoutPosition("*..." term) "]" : term
 
 macro_rules
   | `($c[*...*]) => `(Slice.mk $c *..*)