Idris2Doc : Data.SnocList.Operations

Data.SnocList.Operations

Operations on `SnocList`s, analogous to the `List` ones.
Depending on your style of programming, these might cause
ambiguities, so import with care

Definitions

takeTail : Nat->SnocLista->SnocLista
  Take `n` last elements from `sx`, returning the whole list if
`n` >= length `sx`.

@ n the number of elements to take
@ sx the snoc-list to take the elements from

Totality: total
Visibility: public export
dropTail : Nat->SnocLista->SnocLista
  Remove `n` last elements from `xs`, returning the empty list if
`n >= length xs`

@ n the number of elements to remove
@ xs the list to drop the elements from

Totality: total
Visibility: public export
concatDropTailTakeTail : (n : Nat) -> (sx : SnocLista) ->dropTailnsx++takeTailnsx=sx
Totality: total
Visibility: public export
splitOntoLeft : Nat->SnocLista->Lista-> (SnocLista, Lista)
  Shift `n` elements from the beginning of `xs` to the end of `sx`,
returning the same lists if `n` >= length `xs`.

@ n the number of elements to take
@ sx the snoc-list to append onto
@ xs the list to take the elements from

Totality: total
Visibility: public export
splitOntoRight : Nat->SnocLista->Lista-> (SnocLista, Lista)
  Shift `n` elements from the end of `sx` to the beginning of `xs`,
returning the same lists if `n` >= length `sx`.

@ n the number of elements to take
@ sx the snoc-list to take the elements from
@ xs the list to append onto

Totality: total
Visibility: public export
splitOntoRightInvariant : (n : Nat) -> (sx : SnocLista) -> (xs : Lista) ->fst (splitOntoRightnsxxs) <><snd (splitOntoRightnsxxs) =sx<><xs
Totality: total
Visibility: export
splitOntoRightSpec : (n : Nat) -> (sx : SnocLista) -> (xs : Lista) -> (fst (splitOntoRightnsxxs) =dropTailnsx, snd (splitOntoRightnsxxs) =takeTailnsx<>>xs)
Totality: total
Visibility: export
splitOntoLeftSpec : (n : Nat) -> (sx : SnocLista) -> (xs : Lista) -> (fst (splitOntoLeftnsxxs) =sx<><takenxs, snd (splitOntoLeftnsxxs) =dropnxs)
Totality: total
Visibility: export
lengthHomomorphism : (sx : SnocLista) -> (sy : SnocLista) ->length (sx++sy) =lengthsx+lengthsy
Totality: total
Visibility: export
take : Nat->SnocLista->SnocLista
  Take `n` first elements from `sx`, returning the whole list if
`n` >= length `sx`.

@ n the number of elements to take
@ sx the snoc-list to take the elements from

Note: traverses the whole the input list, so linear in `n` and
`length sx`

Totality: total
Visibility: public export
drop : Nat->SnocLista->SnocLista
  Drop `n` first elements from `sx`, returning an empty list if
`n` >= length `sx`.

@ n the number of elements to drop
@ sx the snoc-list to drop the elements from

Note: traverses the whole the input list, so linear in `n` and
`length sx`

Totality: total
Visibility: public export
dataNonEmpty : SnocLista->Type
Totality: total
Visibility: public export
Constructor: 
IsSnoc : NonEmpty (sx:<x)
last : (sx : SnocLista) -> {auto0_ : NonEmptysx} ->a
Totality: total
Visibility: public export
intersectBy : (a->a->Bool) ->SnocLista->SnocLista->SnocLista
Totality: total
Visibility: public export
intersect : Eqa=>SnocLista->SnocLista->SnocLista
Totality: total
Visibility: public export