Idris2Doc : Data.List1

Data.List1

(++) : List1 a -> List1 a -> List1 a
  Totality: total
  Fixity Declaration: infixr operator, level 7
record List1 : Type -> Type
  Non-empty lists.

  Totality: total
  Constructor: 
(:::) : a -> List a -> List1 a

  Projections:
  
.head : List1 a -> a
  
.tail : List1 a -> List a
appendl : List1 a -> List a -> List1 a
  Totality: total
cons : a -> List1 a -> List1 a
  Totality: total
consInjective : x ::: xs = y ::: ys -> (x = y, xs = ys)
  Totality: total
foldl1 : (a -> a -> a) -> List1 a -> a
  Totality: total
foldl1By : (b -> a -> b) -> (a -> b) -> List1 a -> b
  Totality: total
foldr1 : (a -> a -> a) -> List1 a -> a
  Totality: total
foldr1By : (a -> b -> b) -> (a -> b) -> List1 a -> b
  Totality: total
forget : List1 a -> List a
  Forget that a list is non-empty.

  Totality: total
fromList : List a -> Maybe (List1 a)
  Totality: total
init : List1 a -> List a
  Totality: total
lappend : List a -> List1 a -> List1 a
  Totality: total
last : List1 a -> a
  Totality: total
reverse : List1 a -> List1 a
  Totality: total
reverseOnto : List1 a -> List a -> List1 a
  Totality: total
singleton : a -> List1 a
  Totality: total
snoc : List1 a -> a -> List1 a
  Totality: total
unsnoc : List1 a -> (List a, a)
  Totality: total