Data.DiffList

Definitions

data IsSuffixOf : List a -> List a -> Type

Totality: total
Visibility: public export
Constructors:

SuffixRefl : IsSuffixOf xs xs

ConsSuffix : IsSuffixOf xs ys -> IsSuffixOf xs (y :: ys)

Hints:

Preorder (List a) IsSuffixOf

Reflexive (List a) IsSuffixOf

Transitive (List a) IsSuffixOf

appendIsSuffix : (xs : List a) -> (ys : List a) -> IsSuffixOf ys (xs ++ ys)

Visibility: export

suffixLengthLTE : (xs : List a) -> (ys : List a) -> IsSuffixOf xs ys -> LTE (length xs) (length ys)

Visibility: export

record DiffList : Type -> Type

  A diff-list takes a list, and appends new elements on the front
  This allows for cheap concatenation, no matter how it is associated
  
  This implementation includes a proof that the function can only append
  elements to the front

Totality: total
Visibility: public export
Constructor: 

MkDiffList : (append : (List a -> List a)) -> (0 _ : ((rest : List a) -> IsSuffixOf rest (append rest))) -> DiffList a

Projections:

.append : DiffList a -> List a -> List a

0 .isSuffix : ({rec:0} : DiffList a) -> (rest : List a) -> IsSuffixOf rest (append {rec:0} rest)

Hints:

Monoid (DiffList a)

Semigroup (DiffList a)

.append : DiffList a -> List a -> List a

Visibility: public export

append : DiffList a -> List a -> List a

Visibility: public export

0 .isSuffix : ({rec:0} : DiffList a) -> (rest : List a) -> IsSuffixOf rest (append {rec:0} rest)

Visibility: public export

0 isSuffix : ({rec:0} : DiffList a) -> (rest : List a) -> IsSuffixOf rest (append {rec:0} rest)

Visibility: public export

Nil : DiffList a

Visibility: public export

(::) : a -> DiffList a -> DiffList a

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

toList : DiffList a -> List a

Visibility: public export

diffAppendIsSuffix : (xs : DiffList a) -> (ys : DiffList a) -> (rest : List a) -> IsSuffixOf rest (xs .append (ys .append rest))

singleton : a -> DiffList a

Visibility: public export

fromList : List a -> DiffList a

Visibility: public export

DiffListEq : DiffList a -> DiffList a -> Type

  Equality of `DiffList`s is represented as equality of `DiffList.toList` of each side

Visibility: public export

(.==) : DiffList a -> DiffList a -> Type

Visibility: public export
Fixity Declaration: infix operator, level 6

semigroupAssoc : (xs : DiffList a) -> (ys : DiffList a) -> (zs : DiffList a) -> ((xs <+> ys) <+> zs) .== (xs <+> (ys <+> zs))

Visibility: export

toListFromListId : (xs : List a) -> toList (fromList xs) = xs

Visibility: export

semigroupNilRightNeutral : (xs : DiffList a) -> (xs <+> []) .== xs

Visibility: export

semigroupNilLeftNeutral : (xs : DiffList a) -> ([] <+> xs) .== xs

Visibility: export