Merge branch 'master' of github.com:idris-lang/Idris-dev
commitcd8fe96fc956f8cc73ca60c75d21c0d52eb3452e
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 12 Dec 2013, 10:10 (13 years ago)
parent2e570a350e9624
libs/prelude/Prelude/List.idr−4
@@ -464,10 +464,6 @@ sort xs =
464464-- Conversions
465465--------------------------------------------------------------------------------
466466
467−maybeToList : Maybe a -> List a
468−maybeToList Nothing = []
469−maybeToList (Just j) = [j]
470−
471467listToMaybe : List a -> Maybe a
472468listToMaybe [] = Nothing
473469listToMaybe (x::xs) = Just x