reformulate sep

Main.lean

@@ -14,14 +14,14 @@ def String.replicate : Nat → Char → String
 | 0,   _ => ""
 | n+1, x => replicate n x |>.push x
 
-def sep (xs space : Array String)
+def sep (xs : Array String) (space : Fin (xs.size-1) → String)
   : String := Id.run do
   let mut out := ""
   let mut i := 0
   while h : i < xs.size do
     out := out ++ xs[i]
-    if let some space := space[i]?
-    then out := out ++ space
+    if h : i < xs.size - 1 then
+      out := out ++ space ⟨i, h⟩
     i := i + 1
   return out
 
@@ -34,11 +34,9 @@ def justify : Nat → Array String → String
     let smallSpaceLen := spacesNeeded / numSpaces
     let smallSpace    := String.replicate smallSpaceLen ' '
     let largeSpaces   := spacesNeeded % numSpaces
-    let smallSpaces   := numSpaces - largeSpaces
     let largeSpace    := smallSpace.push ' '
-    let spaces := Array.mkArray largeSpaces largeSpace
-               ++ Array.mkArray smallSpaces smallSpace
-    sep words spaces
+    let space i := if i.val ≤ largeSpaces then largeSpace else smallSpace
+    sep words space
 
 def breakUp (width : Nat) (words : Array String) : Array (Array String) :=
   let (_, line, lines) := words.foldl