Libraries.Data.List.Thin

Definitions

data Thin : List a -> List a -> Type

Totality: total
Visibility: public export
Constructors:

Refl : Thin xs xs

Drop : Thin xs ys -> Thin xs (y :: ys)

Keep : Thin xs ys -> Thin (x :: xs) (x :: ys)

none : Thin [] xs

Totality: total
Visibility: export

keep : Thin xs ys -> Thin (x :: xs) (x :: ys)

  Smart constructor. We should use this to maximise the length
  of the Refl segment thus getting more short-circuiting behaviours

Totality: total
Visibility: export

keeps : (args : List a) -> Thin xs ys -> Thin (args ++ xs) (args ++ ys)

Totality: total
Visibility: export

fromNatSet : NatSet -> (xs : List a) -> (xs' : List a ** Thin xs' xs)

Totality: total
Visibility: export