File tree Expand file tree Collapse file tree 1 file changed +2
-13
lines changed Expand file tree Collapse file tree 1 file changed +2
-13
lines changed Original file line number Diff line number Diff line change @@ -14,17 +14,6 @@ section Utils
1414 else
1515 (a, b ++ .replicate (a.length - b.length) unit)
1616
17- namespace Array
18- def join (xss : Array (Array α)) : Array α := Id.run do
19- let mut r := #[]
20- for xs in xss do
21- r := r ++ xs
22- return r
23-
24- def flatMap (f : α → Array β) (xs : Array α) : Array β :=
25- join (xs.map f)
26- end Array
27-
2817 namespace String
2918 /--
3019 Inserts newlines `\n` into `s` after every `maxWidth` characters so that the result
@@ -150,13 +139,13 @@ section Utils
150139 let rows : Array (List String × String) := rows.map fun (left, right) =>
151140 (maxWidth - margin - minRightColumnWidth |> String.wrapWordsAt! left |>.splitOn "\n " , right)
152141 let leftColumnWidth :=
153- flatMap (·.1 .map (·.length) |>.toArray) rows
142+ rows. flatMap (·.1 .map (·.length) |>.toArray)
154143 |>.getMax? (· < ·)
155144 |>.get!
156145 let leftColumnWidth := leftColumnWidth + margin
157146 let rows : Array (List String × List String) := rows.map fun (left, right) =>
158147 (left, maxWidth - leftColumnWidth |> String.wrapWordsAt! right |>.splitOn "\n " )
159- let rows : Array (String × String) := flatMap (xs := rows) fun (left, right) =>
148+ let rows : Array (String × String) := rows.flatMap fun (left, right) =>
160149 let (left, right) : List String × List String := List.matchLength left right ""
161150 left.zip right |>.toArray
162151 let rows : Array String := rows.map fun (left, right) =>
You can’t perform that action at this time.
0 commit comments