
  0 | module Data.Refined.List
  1 | 
  2 | import public Data.List
  3 | import public Data.List.Quantifiers
  4 | import public Data.Refined.Core
  5 | 
  6 | %default total
  7 | 
  8 | public export
  9 | 0 Len : (p : Nat -> Type) -> List a -> Type
 10 | Len p =  p `On` length
 11 | 
 12 | public export
 13 | HDec0 (List a) NonEmpty where
 14 |   hdec0 (_ :: _) = Just0 %search
 15 |   hdec0 []       = Nothing0
 16 | 
 17 | public export %inline
 18 | HDec (List a) NonEmpty where
 19 |   hdec (_ :: _) = Just %search
 20 |   hdec []       = Nothing
 21 |