Some multiplicity fixes in the libraries

libs/base/Data/Vect.idr

@@ -265,20 +265,6 @@ zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
 zipWith f []      []      = []
 zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
 
-||| Linear version
-public export
-lzipWith : (f : a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
-lzipWith _ [] [] = []
-lzipWith f (x::xs) (y::ys) = f x y :: lzipWith f xs ys
-
-||| Extensional correctness lemma
-export
-lzipWithSpec : (f : a -> b -> c)
-         -> (xs : Vect n a) -> (ys : Vect n b)
-         -> lzipWith f xs ys = zipWith f xs ys
-lzipWithSpec _ [] [] = Refl
-lzipWithSpec f (_::xs) (_::ys) = rewrite lzipWithSpec f xs ys in Refl
-
 ||| Combine three equal-length vectors into a vector with some function
 |||
 ||| ```idris example
@@ -828,21 +814,7 @@ range {len=S _} = FZ :: map FS range
 public export
 transpose : {n : _} -> (array : Vect m (Vect n elem)) -> Vect n (Vect m elem)
 transpose []        = replicate _ []                 -- = [| [] |]
-transpose (x :: xs) = lzipWith (::) x (transpose xs) -- = [| x :: xs |]
-
-||| A recursive (non-linear) implementation of transpose
-||| Easier for inductive reasoning
-public export
-transpose' : {n : Nat} -> (xss : Vect m (Vect n x)) -> Vect n (Vect m x)
-transpose' []          = replicate _ []
-transpose' (xs :: xss) = zipWith (::) xs (transpose' xss)
-
-||| Extensional correctness lemma
-export
-transposeSpec : {n : Nat} -> (xss : Vect m (Vect n x)) -> transpose xss = transpose' xss
-transposeSpec [] = Refl
-transposeSpec (y :: xs) = rewrite transposeSpec xs in
-                          lzipWithSpec (::) _ _
+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
 
 --------------------------------------------------------------------------------
 -- Applicative/Monad/Traversable

libs/contrib/Data/List/Lazy.idr

@@ -8,7 +8,7 @@ module Data.List.Lazy
 public export
 data LazyList : Type -> Type where
   Nil : LazyList a
-  (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
+  (::) : (x : a) -> (xs : Lazy (LazyList a)) -> LazyList a
 
 --- Interface implementations ---
 

libs/contrib/Data/String/Iterator.idr

@@ -29,7 +29,7 @@ fromString : (str : String) -> StringIterator str
 -- This function uses a linear string iterator
 -- so that backends can use mutating iterators.
 export
-withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
+withString : (str : String) -> ((it : StringIterator str) -> a) -> a
 withString str f = f (fromString str)
 
 -- We use a custom data type instead of Maybe (Char, StringIterator)
@@ -51,13 +51,13 @@ data UnconsResult : String -> Type where
   "scheme:blodwen-string-iterator-next"
   "javascript:stringIterator:next"
 export
-uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
+uncons : (str : String) -> (it : StringIterator str) -> UnconsResult str
 
 export
 foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
 foldl op acc str = withString str (loop acc)
   where
-    loop : accTy -> (1 it : StringIterator str) -> accTy
+    loop : accTy -> (it : StringIterator str) -> accTy
     loop acc it =
       case uncons str it of
         EOF => acc
@@ -67,7 +67,7 @@ export
 unpack : String -> LazyList Char
 unpack str = withString str unpack'
   where
-    unpack' : (1 it : StringIterator str) -> LazyList Char
+    unpack' : (it : StringIterator str) -> LazyList Char
     unpack' it =
       case uncons str it of
         EOF => []