Idris2Doc : Data.List1.Properties

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

importpublic Data.Maybe

Definitions

consInjective : x:::xs=y:::ys-> (x=y, xs=ys)
Totality: total
Visibility: export
listLength : (xs : List1a) ->lengthxs=length (forgetxs)
  Proof that the length of a List1 is the same as the length
of the List it represents.

Totality: total
Visibility: export
appendlNilRightNeutral : (l : List1a) ->appendll [] =l
Totality: total
Visibility: export
lappendNilLeftNeutral : (l : List1a) ->lappend [] l=l
Totality: total
Visibility: export
appendAssociative : (l : List1a) -> (c : List1a) -> (r : List1a) ->l++ (c++r) = (l++c) ++r
Totality: total
Visibility: export
toListAppendl : (xs : List1a) -> (ys : Lista) ->toList (appendlxsys) =forgetxs++ys
Totality: total
Visibility: export
toListLappend : (xs : Lista) -> (ys : List1a) ->toList (lappendxsys) =xs++forgetys
Totality: total
Visibility: export
toListAppend : (xs : List1a) -> (ys : List1a) ->toList (xs++ys) =toListxs++toListys
Totality: total
Visibility: export
fromListAppend : (xs : Lista) -> (ys : Lista) ->fromList (xs++ys) =fromListxs<+>fromListys
Totality: total
Visibility: export