Idris2Doc : Data.List.Alternating

Data.List.Alternating

Definitions

dataOdd : 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->Evenba->Oddab

Hints:
Monoida=>Alternative (Odda)
Monoida=>Applicative (Odda)
BifoldableOdd
BifunctorOdd
BitraversableOdd
Eqa=>Eqb=>Eq (Oddab)
Foldable (Odda)
Functor (Odda)
Monoida=>Monoid (Oddab)
Orda=>Ordb=>Ord (Oddab)
Semigroupa=>Semigroup (Oddab)
Showa=>Showb=>Show (Oddab)
Traversable (Odda)
dataEven : 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 : Evenab
(::) : a->Oddba->Evenab

Hints:
BifoldableEven
BifunctorEven
BitraversableEven
Eqa=>Eqb=>Eq (Evenab)
Monoid (Evenab)
Orda=>Ordb=>Ord (Evenab)
Semigroup (Evenab)
Showa=>Showb=>Show (Evenab)
(++) : Oddab->Oddba->Evenab
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
(++) : Evenab->Oddab->Oddab
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
(++) : Evenab->Evenab->Evenab
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
(++) : Oddab->Evenba->Oddab
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
(+>) : Semigroupa=>Oddab->a->Oddab
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5
(<+) : Semigroupa=>a->Oddab->Oddab
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5
singleton : a->Oddab
Totality: total
Visibility: public export
flatten : Odd (Oddab) b->Oddab
Totality: total
Visibility: public export
(>>=) : Monoida=>Oddab-> (b->Oddac) ->Oddac
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
(>>=) : Oddac-> (a->Oddbc) ->Oddbc
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1
odds : Oddab->Lista
Totality: total
Visibility: public export
evens : Evenab->Listb
Totality: total
Visibility: public export
evens : Oddab->Listb
Totality: total
Visibility: public export
odds : Evenab->Lista
Totality: total
Visibility: public export
forget : Oddaa->Lista
Totality: total
Visibility: public export
forget : Evenaa->Lista
Totality: total
Visibility: public export