Data.List1

Reexports

Definitions

record List1 : Type -> Type

  Non-empty lists.

Totality: total
Visibility: public export
Constructor: 

(:::) : a -> List a -> List1 a

Projections:

.head : List1 a -> a

.tail : List1 a -> List a

Hints:

Applicative List1

Biinjective (:::)

DecEq a => DecEq (List1 a)

Eq a => Eq (List1 a)

Foldable List1

Functor List1

Injective (\{arg:0} => x ::: {arg:0})

Injective (\{arg:0} => {arg:0} ::: ys)

Monad List1

Ord a => Ord (List1 a)

Semigroup (List1 a)

Show a => Show (List1 a)

Traversable List1

Uninhabited a => Uninhabited (List1 a)

Zippable List1

.head : List1 a -> a

Totality: total
Visibility: public export

head : List1 a -> a

Totality: total
Visibility: public export

.tail : List1 a -> List a

Totality: total
Visibility: public export

tail : List1 a -> List a

Totality: total
Visibility: public export

fromList : List a -> Maybe (List1 a)

Totality: total
Visibility: public export

singleton : a -> List1 a

Totality: total
Visibility: public export

forget : List1 a -> List a

  Forget that a list is non-empty.

Totality: total
Visibility: public export

last : List1 a -> a

Totality: total
Visibility: export

init : List1 a -> List a

Totality: total
Visibility: export

foldr1By : (a -> b -> b) -> (a -> b) -> List1 a -> b

Totality: total
Visibility: public export

foldl1By : (b -> a -> b) -> (a -> b) -> List1 a -> b

Totality: total
Visibility: public export

foldr1 : (a -> a -> a) -> List1 a -> a

Totality: total
Visibility: public export

foldl1 : (a -> a -> a) -> List1 a -> a

Totality: total
Visibility: public export

length : List1 a -> Nat

Totality: total
Visibility: public export

appendl : List1 a -> List a -> List1 a

Totality: total
Visibility: public export

(++) : List1 a -> List1 a -> List1 a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

lappend : List a -> List1 a -> List1 a

Totality: total
Visibility: public export

cons : a -> List1 a -> List1 a

Totality: total
Visibility: public export

snoc : List1 a -> a -> List1 a

Totality: total
Visibility: public export

unsnoc : List1 a -> (List a, a)

Totality: total
Visibility: public export

reverseOnto : List1 a -> List a -> List1 a

Totality: total
Visibility: public export

reverse : List1 a -> List1 a

Totality: total
Visibility: public export

filter : (a -> Bool) -> List1 a -> Maybe (List1 a)

Totality: total
Visibility: public export