[cleanup] Remove half of Libraries.Data.List1

src/Idris/Error.idr

@@ -15,18 +15,21 @@ import Idris.Pretty
 import Parser.Source
 
 import Data.List
-import Libraries.Data.List1 as Lib
-import Libraries.Data.List.Extra
+import Data.List1
 import Data.Maybe
 import Data.Stream
 import Data.Strings
+
+import Libraries.Data.List.Extra
+import Libraries.Data.List1 as Lib
 import Libraries.Data.String.Extra
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
-import System.File
 import Libraries.Utils.String
 import Libraries.Data.String.Extra
 
+import System.File
+
 %hide Data.Strings.lines
 %hide Data.Strings.lines'
 %hide Data.Strings.unlines

src/Idris/SetOptions.idr

@@ -7,7 +7,6 @@ import Core.Options
 import Core.Unify
 import Libraries.Utils.Path
 import Libraries.Data.List.Extra
-import Libraries.Data.List1 as Lib
 
 import Idris.CommandLine
 import Idris.Package.Types
@@ -18,9 +17,12 @@ import Idris.Version
 import IdrisPaths
 
 import Data.List
+import Data.List1
 import Data.So
 import Data.Strings
 
+import Libraries.Data.List1 as Lib
+
 import System
 import System.Directory
 

src/Libraries/Data/List1.idr

@@ -1,17 +1,9 @@
 module Libraries.Data.List1
 
-import public Data.List1
+import Data.List1
 
 %default total
 
--- TODO: Remove this, once Data.List1.fromList from base is available
---       to the compiler
-
-public export
-fromList : List a -> Maybe (List1 a)
-fromList [] = Nothing
-fromList (x :: xs) = Just (x ::: xs)
-
 -- TODO: Remove this, once Data.List1.unsnoc from base is available
 --       to the compiler
 export

src/TTImp/Utils.idr

@@ -6,9 +6,9 @@ import Core.TT
 import TTImp.TTImp
 
 import Data.List
+import Data.List1
 import Data.Strings
 
-import Libraries.Data.List1 as Lib
 import Libraries.Utils.String
 
 %default covering
@@ -87,8 +87,8 @@ findUniqueBindableNames fc arg env used t
                                 -- toplevel declaration
                                  Hole _ _ => Nothing
                                  _ => pure n
-                    pure $ MkPair n <$> Lib.fromList ns
-            whenJust (Lib.fromList ns) $ recordWarning . ShadowingGlobalDefs fc
+                    pure $ MkPair n <$> fromList ns
+            whenJust (fromList ns) $ recordWarning . ShadowingGlobalDefs fc
        pure assoc
 
 export