- (++) : SnocList a -> SnocList a -> SnocList a
- Totality: total
Fixity Declaration: infixr operator, level 7 - (<><) : SnocList a -> List a -> SnocList a
'fish': Action of lists on snoc-lists
Totality: total
Fixity Declaration: infixl operator, level 7- (<>>) : SnocList a -> List a -> List a
'chips': Action of snoc-lists on lists
Totality: total
Fixity Declaration: infixr operator, level 6- data InBounds : Nat -> SnocList 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
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
- asList : SnocList type -> List type
Transform to a list but keeping the contents in the spine order (term depth).
Totality: total- elem : Eq a => a -> SnocList a -> Bool
Check if something is a member of a snoc-list using the default Boolean equality.
Totality: total- find : (a -> Bool) -> SnocList a -> Maybe a
Find the first element of the snoc-list that satisfies the predicate.
Totality: total- findIndex : (a -> Bool) -> (xs : SnocList a) -> Maybe (Fin (length xs))
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 : SnocList a -> Bool
True iff input is Lin
Totality: total- isSnoc : SnocList a -> Bool
True iff input is (:<)
Totality: total- length : SnocList a -> Nat
- Totality: total