Idris2Doc : Data.SnocList

# Data.SnocList

```A Reversed List
```

## Definitions

`asList : SnocList type -> List type`
`  Transform to a list but keeping the contents in the spine order (term depth).`

Totality: total
Visibility: public export
`isLin : SnocList a -> Bool`
`  True iff input is Lin`

Totality: total
Visibility: public export
`isSnoc : SnocList a -> Bool`
`  True iff input is (:<)`

Totality: total
Visibility: public export
`spanBy : (a -> Maybe b) -> SnocList a -> (SnocList a, SnocList b)`
`  Given a predicate and a snoclist, returns a tuple consisting of the longest  prefix of the snoclist whose elements satisfy the predicate, and the rest of the  snoclist.`

Totality: total
Visibility: public export
`SnocBiinjective : Biinjective (:<)`
Totality: total
Visibility: export
`find : (a -> Bool) -> SnocList a -> Maybe a`
`  Find the rightmost element of the snoc-list that satisfies the predicate.`

Totality: total
Visibility: public export
`data InBounds : Nat -> SnocList a -> Type`
`  Satisfiable if `k` is a valid index into `xs`.    @ k the potential index  @ xs the snoc-list into which k may be an index`

Totality: total
Visibility: public export
Constructors:
`InFirst : InBounds 0 (xs :< x)`
`  Z is a valid index into any cons cell`
`InLater : InBounds k xs -> InBounds (S k) (xs :< x)`
`  Valid indices can be extended`
`findIndex : (a -> Bool) -> (xs : SnocList a) -> Maybe (Fin (length xs))`
`  Find the index (counting from right) of the rightmost element (if exists) of a  snoc-list that satisfies the given test, else `Nothing`.`

Totality: total
Visibility: public export
`appendAssociative : (l : SnocList a) -> (c : SnocList a) -> (r : SnocList a) -> l ++ (c ++ r) = (l ++ c) ++ r`
Totality: total
Visibility: export
`appendLinLeftNeutral : (sx : SnocList a) -> [<] ++ sx = sx`
Totality: total
Visibility: export
`fishAsSnocAppend : (xs : SnocList a) -> (ys : List a) -> xs <>< ys = xs ++ cast ys`
Totality: total
Visibility: export
`chipsAsListAppend : (xs : SnocList a) -> (ys : List a) -> xs <>> ys = cast xs ++ ys`
Totality: total
Visibility: export
`toListAppend : (sx : SnocList a) -> (sy : SnocList a) -> toList (sx ++ sy) = toList sx ++ toList sy`
Totality: total
Visibility: export
`castListAppend : (xs : List a) -> (ys : List a) -> cast (xs ++ ys) = cast xs ++ cast ys`
Totality: total
Visibility: export
`castToList : (sx : SnocList a) -> cast (toList sx) = sx`
Totality: total
Visibility: export
`toListCast : (xs : List a) -> toList (cast xs) = xs`
Totality: total
Visibility: export
`cons : a -> SnocList a -> SnocList a`
`  Append an element to the head of a snoc-list.  Note: Traverses the snoc-list, linear time complexity`

Totality: total
Visibility: public export
`foldAppend : (f : (acc -> a -> acc)) -> (init : acc) -> (sx : SnocList a) -> (sy : SnocList a) -> foldl f init (sx ++ sy) = foldl f (foldl f init sx) sy`
Totality: total
Visibility: export
`snocFoldlAsListFoldl : (f : (acc -> a -> acc)) -> (init : acc) -> (xs : SnocList a) -> foldl f init xs = foldl f init (toList xs)`
Totality: total
Visibility: export
`filterAppend : (f : (a -> Bool)) -> (sx : SnocList a) -> (sy : SnocList a) -> filter f (sx ++ sy) = filter f sx ++ filter f sy`
Totality: total
Visibility: export
`toListFilter : (f : (a -> Bool)) -> (sx : SnocList a) -> toList (filter f sx) = filter f (toList sx)`
Totality: total
Visibility: export
`filterCast : (f : (a -> Bool)) -> (xs : List a) -> filter f (cast xs) = cast (filter f xs)`
Totality: total
Visibility: export
`mapFusion : (g : (b -> c)) -> (f : (a -> b)) -> (sx : SnocList a) -> map g (map f sx) = map (g . f) sx`
Totality: total
Visibility: export
`mapAppend : (f : (a -> b)) -> (sx : SnocList a) -> (sy : SnocList a) -> map f (sx ++ sy) = map f sx ++ map f sy`
Totality: total
Visibility: export
`toListMap : (f : (a -> b)) -> (sx : SnocList a) -> toList (map f sx) = map f (toList sx)`
Totality: total
Visibility: export
`mapCast : (f : (a -> b)) -> (xs : List a) -> map f (cast xs) = cast (map f xs)`
Totality: total
Visibility: export
`mapMaybeFusion : (g : (b -> Maybe c)) -> (f : (a -> Maybe b)) -> (sx : SnocList a) -> mapMaybe g (mapMaybe f sx) = mapMaybe (f >=> g) sx`
Totality: total
Visibility: export
`mapMaybeAppend : (f : (a -> Maybe b)) -> (sx : SnocList a) -> (sy : SnocList a) -> mapMaybe f (sx ++ sy) = mapMaybe f sx ++ mapMaybe f sy`
Totality: total
Visibility: export
`toListMapMaybe : (f : (a -> Maybe b)) -> (sx : SnocList a) -> toList (mapMaybe f sx) = mapMaybe f (toList sx)`
Totality: total
Visibility: export
`mapMaybeCast : (f : (a -> Maybe b)) -> (xs : List a) -> mapMaybe f (cast xs) = cast (mapMaybe f xs)`
Totality: total
Visibility: export