[ fix ] re-export uncons and cleanup Data.String.Base (#1359)

Author: gallais

README/Foreign/Haskell.agda

@@ -81,7 +81,7 @@ eqNat = coerce primIntEq
 
 open import IO
 open import Codata.Musical.Notation
-open import Data.String.Base
+open import Data.String.Base using (toList; fromList; unlines; _++_)
 open import Relation.Nullary.Negation
 
 -- example program using uncons, catMaybes, and testChar

src/Data/String/Base.agda

@@ -11,11 +11,9 @@ module Data.String.Base where
 open import Level using (zero)
 open import Data.Bool.Base using (true; false)
 open import Data.Bool.Properties using (T?)
-open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
-import Data.Nat.Properties as ℕₚ
+open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉; _⊔_)
 open import Data.List.Base as List using (List; [_])
 open import Data.List.NonEmpty as NE using (List⁺)
-open import Data.List.Extrema ℕₚ.≤-totalOrder
 open import Data.List.Relation.Binary.Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Lex.Strict using (Lex-<)
 open import Data.Vec.Base as Vec using (Vec)
@@ -38,7 +36,8 @@ import Agda.Builtin.String as String
 
 open String public using ( String )
   renaming
-  ( primStringToList   to toList
+  ( primStringUncons   to uncons
+  ; primStringToList   to toList
   ; primStringFromList to fromList
   ; primShowString     to show
   )
@@ -174,7 +173,7 @@ rectangle : ∀ {n} → Vec (ℕ → String → String) n →
 rectangle pads cells = Vec.zipWith (λ p c → p width c) pads cells where
 
   sizes = List.map length (Vec.toList cells)
-  width = max 0 sizes
+  width = List.foldr _⊔_ 0 sizes
 
 -- Special cases for left, center, and right alignment