Idris2Doc : Data.List1

Data.List1

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

Totality: total
Constructor: 
(:::) : a -> Lista -> List1a

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

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