Idris2Doc : Data.SnocList

Data.SnocList

A Reversed List
(++) : SnocLista -> SnocLista -> SnocLista
Totality: total
Fixity Declaration: infixr operator, level 7
(<><) : SnocLista -> Lista -> SnocLista
  'fish': Action of lists on snoc-lists

Totality: total
Fixity Declaration: infixl operator, level 7
(<>>) : SnocLista -> Lista -> Lista
  'chips': Action of snoc-lists on lists

Totality: total
Fixity Declaration: infixr operator, level 6
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
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
asList : SnocListtype -> Listtype
  Transform to a list but keeping the contents in the spine order (term depth).

Totality: total
elem : Eqa => a -> SnocLista -> Bool
  Check if something is a member of a snoc-list using the default Boolean equality.

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

Totality: total
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
isLin : SnocLista -> Bool
  True iff input is Lin

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

Totality: total
length : SnocLista -> Nat
Totality: total