Data.List1.Properties

This module contains stuff that may use functions from `Data.List`.
This separation is needed because `Data.List` uses `List1` type inside it,
thus the core of `List1` must not import `Data.List`.

Reexports

Definitions

consInjective : x ::: xs = y ::: ys -> (x = y, xs = ys)

Totality: total
Visibility: export

listLength : (xs : List1 a) -> length xs = length (forget xs)

  Proof that the length of a List1 is the same as the length
  of the List it represents.

Totality: total
Visibility: export

appendlNilRightNeutral : (l : List1 a) -> appendl l [] = l

Totality: total
Visibility: export

lappendNilLeftNeutral : (l : List1 a) -> lappend [] l = l

Totality: total
Visibility: export

appendAssociative : (l : List1 a) -> (c : List1 a) -> (r : List1 a) -> l ++ (c ++ r) = (l ++ c) ++ r

Totality: total
Visibility: export

toListAppendl : (xs : List1 a) -> (ys : List a) -> toList (appendl xs ys) = forget xs ++ ys

Totality: total
Visibility: export

toListLappend : (xs : List a) -> (ys : List1 a) -> toList (lappend xs ys) = xs ++ forget ys

Totality: total
Visibility: export

toListAppend : (xs : List1 a) -> (ys : List1 a) -> toList (xs ++ ys) = toList xs ++ toList ys

Totality: total
Visibility: export

fromListAppend : (xs : List a) -> (ys : List a) -> fromList (xs ++ ys) = fromList xs <+> fromList ys

Totality: total
Visibility: export