Idris2Doc : Data.SnocList

Data.SnocList

A Reversed List

Definitions

asList : SnocListtype->Listtype
  Transform to a list but keeping the contents in the spine order (term depth).

Totality: total
Visibility: public export
isLin : SnocLista->Bool
  True iff input is Lin

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

Totality: total
Visibility: public export
find : (a->Bool) ->SnocLista->Maybea
  Find the first element of the snoc-list that satisfies the predicate.

Totality: total
Visibility: public export
dataInBounds : Nat->SnocLista->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 : InBounds0 (xs:<x)
  Z is a valid index into any cons cell
InLater : InBoundskxs->InBounds (Sk) (xs:<x)
  Valid indices can be extended
findIndex : (a->Bool) -> (xs : SnocLista) ->Maybe (Fin (lengthxs))
  Find the index and proof of InBounds of the first element (if exists) of a
snoc-list that satisfies the given test, else `Nothing`.

Totality: total
Visibility: public export
appendAssociative : (l : SnocLista) -> (c : SnocLista) -> (r : SnocLista) ->l++ (c++r) = (l++c) ++r
Totality: total
Visibility: export
appendLinLeftNeutral : (sx : SnocLista) -> [<] ++sx=sx
Totality: total
Visibility: export
fishAsSnocAppend : (xs : SnocLista) -> (ys : Lista) ->xs<><ys=xs++castys
Totality: total
Visibility: export
chipsAsListAppend : (xs : SnocLista) -> (ys : Lista) ->xs<>>ys=castxs++ys
Totality: total
Visibility: export
toListAppend : (sx : SnocLista) -> (sy : SnocLista) ->toList (sx++sy) =toListsx++toListsy
Totality: total
Visibility: export
castListAppend : (xs : Lista) -> (ys : Lista) ->cast (xs++ys) =castxs++castys
Totality: total
Visibility: export
castToList : (sx : SnocLista) ->cast (toListsx) =sx
Totality: total
Visibility: export
toListCast : (xs : Lista) ->toList (castxs) =xs
Totality: total
Visibility: export
cons : a->SnocLista->SnocLista
  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 : SnocLista) -> (sy : SnocLista) ->foldlfinit (sx++sy) =foldlf (foldlfinitsx) sy
Totality: total
Visibility: export
snocFoldlAsListFoldl : (f : (acc->a->acc)) -> (init : acc) -> (xs : SnocLista) ->foldlfinitxs=foldlfinit (toListxs)
Totality: total
Visibility: export
filterAppend : (f : (a->Bool)) -> (sx : SnocLista) -> (sy : SnocLista) ->filterf (sx++sy) =filterfsx++filterfsy
Totality: total
Visibility: export
toListFilter : (f : (a->Bool)) -> (sx : SnocLista) ->toList (filterfsx) =filterf (toListsx)
Totality: total
Visibility: export
filterCast : (f : (a->Bool)) -> (xs : Lista) ->filterf (castxs) =cast (filterfxs)
Totality: total
Visibility: export
mapFusion : (g : (b->c)) -> (f : (a->b)) -> (sx : SnocLista) ->mapg (mapfsx) =map (g.f) sx
Totality: total
Visibility: export
mapAppend : (f : (a->b)) -> (sx : SnocLista) -> (sy : SnocLista) ->mapf (sx++sy) =mapfsx++mapfsy
Totality: total
Visibility: export
toListMap : (f : (a->b)) -> (sx : SnocLista) ->toList (mapfsx) =mapf (toListsx)
Totality: total
Visibility: export
mapCast : (f : (a->b)) -> (xs : Lista) ->mapf (castxs) =cast (mapfxs)
Totality: total
Visibility: export
mapMaybeFusion : (g : (b->Maybec)) -> (f : (a->Maybeb)) -> (sx : SnocLista) ->mapMaybeg (mapMaybefsx) =mapMaybe (f>=>g) sx
Totality: total
Visibility: export
mapMaybeAppend : (f : (a->Maybeb)) -> (sx : SnocLista) -> (sy : SnocLista) ->mapMaybef (sx++sy) =mapMaybefsx++mapMaybefsy
Totality: total
Visibility: export
toListMapMaybe : (f : (a->Maybeb)) -> (sx : SnocLista) ->toList (mapMaybefsx) =mapMaybef (toListsx)
Totality: total
Visibility: export
mapMaybeCast : (f : (a->Maybeb)) -> (xs : Lista) ->mapMaybef (castxs) =cast (mapMaybefxs)
Totality: total
Visibility: export