Data.Container.Additive.Quantifiers

Definitions

data AllPos : All .Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllPos []

(::) : c .Pos s -> AllPos ss -> AllPos (s :: ss)

head : AllPos (s :: ss) -> c .Pos s

Visibility: public export

tail : AllPos (s :: ss) -> AllPos ss

Visibility: public export

allPosPlus : (s : All .Shp cs) -> AllPos s -> AllPos s -> AllPos s

Visibility: public export

allPosNeutral : (s : All .Shp cs) -> AllPos s

Visibility: public export

allPosComMonoid : (s : All .Shp cs) -> ComMonoid (AllPos s)

Visibility: public export

data AnyShpPos : Any .Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Here : c .Pos s -> AnyShpPos (Here s)

There : AnyShpPos ss -> AnyShpPos (There ss)

anyShpPosPlus : (s : Any .Shp cs) -> AnyShpPos s -> AnyShpPos s -> AnyShpPos s

Visibility: public export

anyShpPosNeutral : (s : Any .Shp cs) -> AnyShpPos s

Visibility: public export

anyShpPosComMonoid : (s : Any .Shp cs) -> ComMonoid (AnyShpPos s)

Visibility: public export

data AllPos : All .Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllPos []

(::) : c .Pos s -> AllPos ss -> AllPos (s :: ss)

head : AllPos (s :: ss) -> c .Pos s

Visibility: public export

tail : AllPos (s :: ss) -> AllPos ss

Visibility: public export

allPosPlus : (s : All .Shp cs) -> AllPos s -> AllPos s -> AllPos s

Visibility: public export

allPosComMonoid : (s : All .Shp cs) -> ComMonoid (AllPos s)

Visibility: public export

data AnyShpPos : Any .Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Here : c .Pos s -> AnyShpPos (Here s)

There : AnyShpPos ss -> AnyShpPos (There ss)

anyShpPosPlus : (s : Any .Shp cs) -> AnyShpPos s -> AnyShpPos s -> AnyShpPos s

Visibility: public export

anyShpPosNeutral : (s : Any .Shp cs) -> AnyShpPos s

Visibility: public export

anyShpPosComMonoid : (s : Any .Shp cs) -> ComMonoid (AnyShpPos s)

Visibility: public export