Data.List.Alternating

Definitions

data Odd : Type -> Type -> Type

  Non-empty list, starting and ending with an a, where adjacent elements alternate
  between types a and b.
  We can think of this type as:
  - A fence, with the `a`s as fence-posts, and the `b`s as panels.
  - A non-empty list of `a`s, separated by `b`s
  - A list of `b`s, separated by, and surrounded by, `a`s
  - The free extension of a monoid `a`, with variables in `b`

Totality: total
Visibility: public export
Constructor: 

(::) : a -> Even b a -> Odd a b

Hints:

Monoid a => Alternative (Odd a)

Monoid a => Applicative (Odd a)

Bifoldable Odd

Bifunctor Odd

Bitraversable Odd

Eq a => Eq b => Eq (Odd a b)

Foldable (Odd a)

Functor (Odd a)

Monoid a => Monoid (Odd a b)

Ord a => Ord b => Ord (Odd a b)

Semigroup a => Semigroup (Odd a b)

Show a => Show b => Show (Odd a b)

Traversable (Odd a)

data Even : Type -> Type -> Type

  A list, starting with an a, and ending with a b; where adjacent elements
  alternate between types a and b.
  Equivalent to List (a, b)

Totality: total
Visibility: public export
Constructors:

Nil : Even a b

(::) : a -> Odd b a -> Even a b

Hints:

Bifoldable Even

Bifunctor Even

Bitraversable Even

Eq a => Eq b => Eq (Even a b)

Monoid (Even a b)

Ord a => Ord b => Ord (Even a b)

Semigroup (Even a b)

Show a => Show b => Show (Even a b)

(++) : Odd a b -> Odd b a -> Even a b

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

(++) : Even a b -> Odd a b -> Odd a b

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

(++) : Even a b -> Even a b -> Even a b

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

(++) : Odd a b -> Even b a -> Odd a b

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

(+>) : Semigroup a => Odd a b -> a -> Odd a b

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

(<+) : Semigroup a => a -> Odd a b -> Odd a b

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5

singleton : a -> Odd a b

Totality: total
Visibility: public export

flatten : Odd (Odd a b) b -> Odd a b

Totality: total
Visibility: public export

(>>=) : Monoid a => Odd a b -> (b -> Odd a c) -> Odd a c

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1

(>>=) : Odd a c -> (a -> Odd b c) -> Odd b c

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1

odds : Odd a b -> List a

Totality: total
Visibility: public export

evens : Even a b -> List b

Totality: total
Visibility: public export

evens : Odd a b -> List b

Totality: total
Visibility: public export

odds : Even a b -> List a

Totality: total
Visibility: public export

forget : Odd a a -> List a

Totality: total
Visibility: public export

forget : Even a a -> List a

Totality: total
Visibility: public export