Libraries.Data.List01

Definitions

data List01 : Bool -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : List01 False a

(::) : a -> List01 ne a -> List01 True a

Hints:

Foldable (List01 ne)

Functor (List01 ne)

Show (Partitions ps)

Show a => Show (List01 ne a)

fromList : (xs : List a) -> List01 (isCons xs) a

Visibility: public export

(++) : List01 nel a -> List01 ner a -> List01 (nel || Delay ner) a

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

length : List01 ne a -> Nat

Visibility: public export

forget : List01 ne a -> List a

Visibility: public export