Data.List.Suffix

Reexports

Definitions

data Suffix : Bool -> List a -> List a -> Type

  Proof that a list is a (possibly strict) suffix of another list.
  
  Performance: Values of this type are optimized to integers at runtime.

Totality: total
Visibility: public export
Constructors:

Same : Suffix False xs xs

  Every list is a (non-strict) suffix of itself.

Uncons : Suffix b (h :: t) cs -> Suffix b2 t cs

  If a non-empty list `xs` is a suffix of `ys`, then the tail of
  `xs` is a strict suffix of `ys`.

Hints:

Cast (Suffix b xs ys) Nat

Reflexive (List a) (Suffix False)

Transitive (List a) (Suffix False)

Transitive (List a) (Suffix True)

Uninhabited (Suffix b (h :: t) [])

Uninhabited (Suffix True xs [])

uncons : Suffix b (h :: t) cs -> Suffix True t cs

  Strict version of `Uncons`

Totality: total
Visibility: public export

toNat : Suffix b xs ys -> Nat

  Converts a `Suffix` to a natural number, representing
  the number of items dropped from the original list.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

swapOr : Suffix (x || Delay y) xs ys -> Suffix (y || Delay x) xs ys

Totality: total
Visibility: public export

orSame : Suffix (x || Delay x) xs ys -> Suffix x xs ys

Totality: total
Visibility: public export

orTrue : Suffix (x || Delay True) xs ys -> Suffix True xs ys

Totality: total
Visibility: public export

orFalse : Suffix (x || Delay False) xs ys -> Suffix x xs ys

Totality: total
Visibility: public export

swapAnd : Suffix (x && Delay y) xs ys -> Suffix (y && Delay x) xs ys

Totality: total
Visibility: public export

andSame : Suffix (x && Delay x) xs ys -> Suffix x xs ys

Totality: total
Visibility: public export

andTrue : Suffix (x && Delay True) xs ys -> Suffix x xs ys

Totality: total
Visibility: public export

andFalse : Suffix (x && Delay False) xs ys -> Suffix False xs ys

Totality: total
Visibility: public export

weaken : Suffix b xs ys -> Suffix False xs ys

  Every `Suffix` can be converted to a non-strict one.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

weakens : Suffix True xs ys -> Suffix b xs ys

  A strict `Suffix` can be converted to a non-strict one.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

unconsBoth : Suffix b (y :: ys) (x :: xs) -> Suffix False ys xs

Totality: total
Visibility: public export

unconsRight : Suffix True ys (x :: xs) -> Suffix False ys xs

Totality: total
Visibility: public export

and1 : Suffix b1 xs ys -> Suffix (b1 && b2) xs ys

Totality: total
Visibility: public export

and2 : Suffix b2 xs ys -> Suffix (b1 && Delay b2) xs ys

Totality: total
Visibility: public export

trans : Suffix b1 xs ys -> Suffix b2 ys cs -> Suffix (b1 || Delay b2) xs cs

  `Suffix` is a reflexive and transitive relation.
  
  Performance: This is integer addition at runtime.

Totality: total
Visibility: public export

data SuffixAcc : List t -> Type

Totality: total
Visibility: public export
Constructor: 

SA : (Suffix True ys ts => SuffixAcc ys) -> SuffixAcc ts

suffixAcc : SuffixAcc ts

Totality: total
Visibility: export

data Link : List a -> List a -> Type

  Syntactic sugar for describing transitive chains of suffixes.

Totality: total
Visibility: public export
Constructors:

F : (0 xs : List {a:2636}) -> {auto 0 _ : Suffix False xs ys} -> Link xs ys

T : (0 xs : List {a:2658}) -> {auto 0 _ : Suffix True xs ys} -> Link xs ys

any : Suffix b xs ys -> Link xs ys

Totality: total
Visibility: public export

data Chain : List a -> List a -> Type

  Syntactic sugar for describing transitive chains of suffixes.

Totality: total
Visibility: public export
Constructors:

Nil : Chain xs xs

(::) : (0 _ : Link xs ys) -> (0 _ : Chain ys zs) -> Chain xs zs

data IsStrict : Chain xs ys -> Type

Totality: total
Visibility: public export
Constructors:

Here : IsStrict (T xs :: ys)

There : IsStrict c -> IsStrict (l :: c)

0 weak : Chain xs ys -> Suffix False xs ys

Totality: total
Visibility: public export

0 strict : (c : Chain xs ys) -> IsStrict c => Suffix True xs ys

Totality: total
Visibility: public export

takePrefix : (ys : List t) -> Suffix b xs ys -> List t

Totality: total
Visibility: public export

packPrefix : Suffix b xs cs -> String

Totality: total
Visibility: public export