
  0 | module Libraries.Data.List01
  1 | 
  2 | import Data.List
  3 | 
  4 | public export
  5 | data List01 : (nonEmpty : Bool) -> Type -> Type where
  6 |   Nil  : List01 False a
  7 |   (::) : a -> List01 ne a -> List01 True a
  8 | 
  9 | public export
 10 | fromList : (xs : List a) -> List01 (isCons xs) a
 11 | fromList [] = []
 12 | fromList (x :: xs) = x :: fromList xs
 13 | 
 14 | public export
 15 | (++) : List01 nel a -> List01 ner a -> List01 (nel || ner) a
 16 | [] ++ ys = ys
 17 | (x :: xs) ++ ys = x :: xs ++ ys
 18 | 
 19 | public export
 20 | length : (xs : List01 ne a) -> Nat
 21 | length [] = 0
 22 | length (_ :: xs) = S (length xs)
 23 | 
 24 | public export
 25 | forget : List01 ne a -> List a
 26 | forget [] = []
 27 | forget (x :: xs) = x :: forget xs
 28 | 
 29 | public export
 30 | Functor (List01 ne) where
 31 |   map f [] = []
 32 |   map f (x :: xs) = f x :: map f xs
 33 | 
 34 | export
 35 | Show a => Show (List01 ne a) where
 36 |     show = show . forget
 37 | 
 38 | export
 39 | Foldable (List01 ne) where
 40 |   foldr c n [] = n
 41 |   foldr c n (x :: xs) = c x (foldr c n xs)
 42 | 
 43 |   foldl f q [] = q
 44 |   foldl f q (x :: xs) = foldl f (f q x) xs
 45 | 
 46 |   null [] = True
 47 |   null (_ :: _) = False
 48 | 
 49 |   toList = forget
 50 | 
 51 |   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
 52 |