From 0706170d9598626d96b596eb4e75ffa453c35d79 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 28 Jan 2025 11:31:50 -0500
Subject: [PATCH] remove `Array.replicate` and `#eval`s

`Array.mkArray` does the same thing. couldn't remember the name!
---
 Main.lean | 26 ++++----------------------
 1 file changed, 4 insertions(+), 22 deletions(-)

diff --git a/Main.lean b/Main.lean
index 647486d..3e26416 100644
--- a/Main.lean
+++ b/Main.lean
@@ -10,19 +10,6 @@ def Array.unlines (xs : Array String) : String := Id.run do
     out := out ++ line ++ "\n"
   return out
 
-def ex := "The heat bloomed\tin December\nas the carnival  season\n        kicked into gear.\nNearly helpless with sun and glare, I avoided Rio's brilliant\nsidewalks\n  and glittering beaches,\npanting in dark   corners\nand waiting out the inverted southern summer."
-
-#eval ex.words
-#eval ex.lines
-#eval IO.println ex.lines.unlines
-
-def Array.replicate : Nat → α → Array α
-| 0,   _ => #[]
-| n+1, x => replicate n x |>.push x
-
-theorem Array.replicate_size_eq_n : (Array.replicate n x).size = n := by
-  induction n <;> simp [Array.replicate, *]
-
 def String.replicate : Nat → Char → String
 | 0,   _ => ""
 | n+1, x => replicate n x |>.push x
@@ -32,9 +19,9 @@ def sep (xs space : Array String)
   let mut out := ""
   let mut i := 0
   while h : i < xs.size do
-    out := out.append xs[i]
+    out := out ++ xs[i]
     if let some space := space[i]?
-    then out := out.append space
+    then out := out ++ space
     i := i + 1
   return out
 
@@ -49,13 +36,10 @@ def justify : Nat → Array String → String
     let largeSpaces   := spacesNeeded % numSpaces
     let smallSpaces   := numSpaces - largeSpaces
     let largeSpace    := smallSpace.push ' '
-    let spaces := Array.replicate largeSpaces largeSpace
-               ++ Array.replicate smallSpaces smallSpace
+    let spaces := Array.mkArray largeSpaces largeSpace
+               ++ Array.mkArray smallSpaces smallSpace
     sep words spaces
 
-#eval justify 1 "Hello, world, how is it going?".words
-#eval justify 1 "Hello, world, how is it going?".words |>.length
-
 def breakUp (width : Nat) (words : Array String) : Array (Array String) :=
   let (_, line, lines) := words.foldl
     (λ(left, line, lines) word ↦
@@ -68,8 +52,6 @@ def breakUp (width : Nat) (words : Array String) : Array (Array String) :=
 def solve (width : Nat) :=
   Array.unlines ∘ Array.map (justify width) ∘ breakUp width ∘ String.words
 
-#eval IO.println $ solve 40 ex
-
 def usage := "Usage: justify WIDTH"
 def fail : IO UInt32 := do IO.println usage; return 1