Data.Queue1

Definitions

record Queue1 : Type -> Type

Totality: total
Visibility: export
Constructor: 

MkQueue : SnocList a -> List1 a -> Queue1 a

Projections:

.left : Queue1 a -> List1 a

.right : Queue1 a -> SnocList a

Hint: 

Functor Queue1

singleton : a -> Queue1 a

Totality: total
Visibility: export

add : a -> Queue1 a -> Queue1 a

Totality: total
Visibility: export

remove : Queue1 a -> (a, Lazy (Maybe (Queue1 a)))

Totality: total
Visibility: export

filter : (a -> Bool) -> Queue1 a -> Maybe (Queue1 a)

Totality: total
Visibility: export

toList1 : Queue1 a -> List1 a

  Returns a `List1` with newly added elements on the right and older elements in the left

Totality: total
Visibility: export