Data.SnocVect

Definitions

data SnocVect : Nat -> Type -> Type

  A Backwards Vect

Totality: total
Visibility: public export
Constructors:

Lin : SnocVect 0 a

  Empty snoc-vect

(:<) : SnocVect n a -> a -> SnocVect (S n) a

  A non-empty snoc-vect, consisting of the rest of the snoc-vect and the final element.

Hints:

Applicative (SnocVect k)

Cast (SnocVect n a) (Vect n a)

Cast (Vect n a) (SnocVect n a)

Eq a => Eq (SnocVect n a)

Foldable (SnocVect n)

Functor (SnocVect n)

Monad (SnocVect k)

Monoid a => Monoid (SnocVect k a)

Ord a => Ord (SnocVect n a)

Semigroup a => Semigroup (SnocVect n a)

Show a => Show (SnocVect n a)

Traversable (SnocVect k)

Zippable (SnocVect k)

(<><) : SnocVect n a -> Vect m a -> SnocVect (n + m) a

  'fish': Action of lists on snoc-lists

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

(<>>) : SnocVect j a -> Vect k a -> Vect (j + k) a

  'chips': Action of snoc-lists on lists

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

asVect : SnocVect n type -> Vect n type

  Transform to a vect but keeping the contents in the spine order (term depth).

Totality: total
Visibility: public export

isLin : SnocVect n a -> Bool

  True iff input is Lin

Totality: total
Visibility: public export

isSnoc : SnocVect n a -> Bool

  True iff input is (:<)

Totality: total
Visibility: public export

(++) : SnocVect j a -> SnocVect k a -> SnocVect (j + k) a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

length : SnocVect n a -> Nat

Totality: total
Visibility: public export

lengthCorrect : (sx : SnocVect n a) -> length sx = n

Totality: total
Visibility: export

replicate : (k : Nat) -> a -> SnocVect k a

Totality: total
Visibility: public export

deah : SnocVect (S n) a -> a

  The "head" of the snoc-vect

Totality: total
Visibility: public export

liat : SnocVect (S n) a -> SnocVect n a

  The "tail" of the snoc-vect

Totality: total
Visibility: public export

diag : SnocVect len (SnocVect len el) -> SnocVect len el

  Get diagonal elements

Totality: total
Visibility: public export

find : (a -> Bool) -> SnocVect k a -> Maybe a

  Find the first element of the snoc-vect that satisfies the predicate.

Totality: total
Visibility: public export

data InBounds : Nat -> SnocVect j 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) -> (sx : SnocVect k a) -> Maybe (Fin (length sx))

  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