Theory.List1

Definitions

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

  Concatenation of non-empty lists os associative

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

map_append : (l : List1 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