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 -> SnocList a -> SnocList a

  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 -> SnocList a -> SnocList a

  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 : SnocList a) -> dropTail n sx ++ takeTail n sx = sx

Totality: total
Visibility: public export

splitOntoLeft : Nat -> SnocList a -> List a -> (SnocList a, List a)

  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 -> SnocList a -> List a -> (SnocList a, List a)

  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 : SnocList a) -> (xs : List a) -> fst (splitOntoRight n sx xs) <>< snd (splitOntoRight n sx xs) = sx <>< xs

Totality: total
Visibility: export

splitOntoRightSpec : (n : Nat) -> (sx : SnocList a) -> (xs : List a) -> (fst (splitOntoRight n sx xs) = dropTail n sx, snd (splitOntoRight n sx xs) = takeTail n sx <>> xs)

Totality: total
Visibility: export

splitOntoLeftSpec : (n : Nat) -> (sx : SnocList a) -> (xs : List a) -> (fst (splitOntoLeft n sx xs) = sx <>< take n xs, snd (splitOntoLeft n sx xs) = drop n xs)

Totality: total
Visibility: export

lengthHomomorphism : (sx : SnocList a) -> (sy : SnocList a) -> length (sx ++ sy) = length sx + length sy

Totality: total
Visibility: export

take : Nat -> SnocList a -> SnocList a

  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 -> SnocList a -> SnocList a

  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

data NonEmpty : SnocList a -> Type

Totality: total
Visibility: public export
Constructor: 

IsSnoc : NonEmpty (sx :< x)

last : (sx : SnocList a) -> {auto 0 _ : NonEmpty sx} -> a

Totality: total
Visibility: public export

intersectBy : (a -> a -> Bool) -> SnocList a -> SnocList a -> SnocList a

Totality: total
Visibility: public export

intersect : Eq a => SnocList a -> SnocList a -> SnocList a

Totality: total
Visibility: public export