Theory.List

Definitions

concat_assoc : (l : List a) -> (l' : List a) -> (l'' : List a) -> l ++ (l' ++ l'') = (l ++ l') ++ l''

  Concatenation of lists os associative

Totality: total
Visibility: export

concat_nil : (l : List a) -> l ++ [] = l

  Concatenating a list with an emoty list results in the same list

Totality: total
Visibility: export

map_concat : (l : List a) -> (l' : List a) -> map f (l ++ l') = map f l ++ map f l'

  The mapping of a function on a concatenation of two lists
  is the concatenation of mappings of that function on those lists

Totality: total
Visibility: export

map_append : (l : List a) -> (x : a) -> map f (l ++ [x]) = map f l ++ [f x]

  `map_concat` in the case when the right operand is a singleton

Totality: total
Visibility: export

nonempty_concat_left' : (xs : List a) -> (ys : List a) -> NonEmpty xs -> NonEmpty (xs ++ ys)

  The concatenation of a non-empty list with another list is non-empty

Totality: total
Visibility: export

nonempty_concat_left : NonEmpty xs -> NonEmpty (xs ++ ys)

  The concatenation of a non-empty list with another list is non-empty

Totality: total
Visibility: export

nonempty_concat_right' : (xs : List a) -> (ys : List a) -> NonEmpty ys -> NonEmpty (xs ++ ys)

  The concatenation of a list with a non-empty list is non-empty

Totality: total
Visibility: export

nonempty_concat_right : NonEmpty ys -> NonEmpty (xs ++ ys)

  The concatenation of a list with a non-empty list is non-empty

Totality: total
Visibility: export

nonempty_flip_concat' : (xs : List a) -> (ys : List a) -> NonEmpty (xs ++ ys) -> NonEmpty (ys ++ xs)

  If   the concatenation of one list  with another is non-empty,
  then the concatenation of the other with the one is non-empty

Totality: total
Visibility: export

nonempty_flip_concat : NonEmpty (xs ++ ys) -> NonEmpty (ys ++ xs)

  If   the concatenation of one list  with another is non-empty,
  then the concatenation of the other with the one is non-empty

Totality: total
Visibility: export

nonempty_map' : (xs : List a) -> (f : (a -> b)) -> NonEmpty xs -> NonEmpty (map f xs)

  If a list is non-empty, then any mapping on that list is also non-empty

Totality: total
Visibility: export

nonempty_map : NonEmpty xs -> NonEmpty (map f xs)

  If a list is non-empty, then any mapping on that list is also non-empty

Totality: total
Visibility: export

nonempty_sublist' : (xs : List a) -> (ys : List a) -> NonEmpty (xs ++ ys) -> Either (NonEmpty xs) (NonEmpty ys)

  If the concatenation of two lists is non-empty, then one of the two lists is non-empty

Totality: total
Visibility: export

nonempty_sublist : NonEmpty (xs ++ ys) -> Either (NonEmpty xs) (NonEmpty ys)

  If the concatenation of two lists is non-empty,
  then one of the two lists is non-empty

Totality: total
Visibility: export

nonempty_concat_map' : (xs : List a) -> (ys : List a) -> (f : (a -> b)) -> (g : (a -> b)) -> NonEmpty (xs ++ ys) -> NonEmpty (map f xs ++ map g ys)

  If   the concatenation of two               lists is non-empty,
  then the concatenation of mappings on those lists is non-empty

Totality: total
Visibility: export

nonempty_concat_map : NonEmpty (xs ++ ys) -> NonEmpty (map f xs ++ map g ys)

  If   the concatenation of two               lists is non-empty,
  then the concatenation of mappings on those lists is non-empty

Totality: total
Visibility: export