diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 79f619769..3bcdfe32d 100644 --- a/src/Idris/Error.idr +++ b/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 diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 13affee5d..0a1553a03 100644 --- a/src/Idris/SetOptions.idr +++ b/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 diff --git a/src/Libraries/Data/List1.idr b/src/Libraries/Data/List1.idr index 2273c6bdf..5dcce8b8d 100644 --- a/src/Libraries/Data/List1.idr +++ b/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 diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index e267af2ea..80ef38208 100644 --- a/src/TTImp/Utils.idr +++ b/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