Idris2Doc : Data.List.Alternating

# 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