From 611cc2a28190ab67172b99f8a1bba6e1b2a44760 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 28 Jan 2025 21:22:16 -0500
Subject: [PATCH] reformulate `sep`
---
Main.lean | 12 +++++-------
1 file changed, 5 insertions(+), 7 deletions(-)
diff --git a/Main.lean b/Main.lean
index ae58106..71f1ed7 100644
--- a/Main.lean
+++ b/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