Data.Container.Base.Quantifiers

Definitions

data AllPos : All Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllPos []

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

data AnyPos : All Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Here : c .Pos s -> AnyPos (s :: ss)

There : AnyPos ss -> AnyPos (s :: ss)

data AnyShpPos : Any Shp cs -> Type

  Once we pick a particular shape, we're forced to pick that position

Totality: total
Visibility: public export
Constructors:

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

There : AnyShpPos ss -> AnyShpPos (There ss)

data AllPos : All Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllPos []

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

data AnyPos : All Shp cs -> Type

Totality: total
Visibility: public export
Constructors:

Here : c .Pos s -> AnyPos (s :: ss)

There : AnyPos ss -> AnyPos (s :: ss)

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)