Data.NEList

(++) : NEList a -> NEList a -> NEList a

Fixity

Left associative, precedence 7

MkNEList : (head : a) -> (tail : List a) -> NEList a

record NEList a

a

 

MkNEList : (head : a) -> (tail : List a) -> NEList a

head : (rec : NEList a) -> a

tail : (rec : NEList a) -> List a

appendopt : NEList a -> Maybe (NEList a) -> NEList a

concat : NEList (NEList a) -> NEList a

cons : a -> NEList a -> NEList a

consopt : a -> Maybe (NEList a) -> NEList a

foldl1 : (a -> a -> a) -> NEList a -> a

foldr1 : (a -> a -> a) -> NEList a -> a

foldrf : (a -> b -> b) -> (a -> b) -> NEList a -> b

fromList : List a -> Maybe (NEList a)

fromVect : Vect (S n) a -> NEList a

length : NEList a -> Nat

optappend : Maybe (NEList a) -> NEList a -> NEList a

singleton : a -> NEList a

toList : NEList a -> List a

toVect : (nel : NEList a) -> Vect (length nel) a