Skip to content

Commit 3496e27

Browse files
committed
remove comments
1 parent b131e8a commit 3496e27

File tree

1 file changed

+0
-14
lines changed

1 file changed

+0
-14
lines changed

src/Init/Data/Slice/Basic.lean

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -25,20 +25,6 @@ structure _root_.Std.Slice (shape : RangeShape) (α : Type u) {β : Type v}
2525
carrier : α
2626
range : PRange shape β
2727

28-
-- syntax:max term noWs "[" withoutPosition("*...*") "]" : term
29-
-- syntax:max term noWs "[" withoutPosition(term "...*") "]" : term
30-
-- syntax:max term noWs "[" withoutPosition("*...*") "]" : term
31-
-- syntax:max term noWs "[" withoutPosition(term "<...*") "]" : term
32-
-- syntax:max term noWs "[" withoutPosition(term "...<" term) "]" : term
33-
-- syntax:max term noWs "[" withoutPosition(term "<...<" term) "]" : term
34-
-- syntax:max term noWs "[" withoutPosition("*...<" term) "]" : term
35-
-- syntax:max term noWs "[" withoutPosition(term "...=" term) "]" : term
36-
-- syntax:max term noWs "[" withoutPosition(term "<...=" term) "]" : term
37-
-- syntax:max term noWs "[" withoutPosition("*...=" term) "]" : term
38-
-- syntax:max term noWs "[" withoutPosition(term "..." term) "]" : term
39-
-- syntax:max term noWs "[" withoutPosition(term "<..." term) "]" : term
40-
-- syntax:max term noWs "[" withoutPosition("*..." term) "]" : term
41-
4228
macro_rules
4329
| `($c[*...*]) => `(Slice.mk $c *...*)
4430
| `($c[$a...*]) => `(Slice.mk $c $a...*)

0 commit comments

Comments
 (0)