Data.TCQueue

Definitions

data Tree : (Type -> Type) -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Leaf : (a -> f b) -> Tree f a b

Node : Tree f a x -> Tree f x b -> Tree f a b

data TCQueue : (Type -> Type) -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Empty : TCQueue f a a

Filled : Tree f a b -> TCQueue f a b

empty : TCQueue f a a

Totality: total
Visibility: public export

singleton : (a -> f b) -> TCQueue f a b

Totality: total
Visibility: public export

cons : (a -> f x) -> TCQueue f x b -> TCQueue f a b

Totality: total
Visibility: public export

snoc : TCQueue f a x -> (x -> f b) -> TCQueue f a b

Totality: total
Visibility: public export

(++) : TCQueue f a x -> TCQueue f x b -> TCQueue f a b

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

data ViewL : (Type -> Type) -> Type -> Type -> Type

  Left-edge deconstruction

Totality: total
Visibility: public export
Constructors:

EmptyV : ViewL f a a

(:|) : (a -> f x) -> TCQueue f x b -> ViewL f a b

uncons : TCQueue f a b -> ViewL f a b

Totality: total
Visibility: public export