Data.Tensor.Shape.Axis

Definitions

AxisName : Type

  The name for an axis is an arbitrary string

Visibility: public export

record Axis : Type

  An axis is a container together with its name

Totality: total
Visibility: public export
Constructor: 

(~>) : AxisName -> Cont -> Axis

Projections:

.cont : Axis -> Cont

.name : Axis -> AxisName

Hint: 

IsNaperian a -> IsNaperian (a .cont)

.name : Axis -> AxisName

Visibility: public export

name : Axis -> AxisName

Visibility: public export

.cont : Axis -> Cont

Visibility: public export

cont : Axis -> Cont

Visibility: public export

rename : Axis -> AxisName -> Axis

Visibility: public export

TTInternalName : AxisName

  In some cases we TensorType might need to assign a default name to an axis,
  one which is internal and will not be exposed to the user.
  This is the default name for such cases

Visibility: public export

(~~>) : AxisName -> Nat -> Axis

  A "constructor" for cubical axes

Visibility: public export
Fixity Declaration: infixr operator, level 0

data IsCubical : Axis -> Type

  Follows the pattern of `IsCubical` from `Base.Object.Definition`

Totality: total
Visibility: public export
Constructor: 

MkIsCubical : (name : AxisName) -> (n : Nat) -> IsCubical (name ~~> n)

Hint: 

All IsCubical shape -> AllC IsFoldable shape

toContCubical : IsCubical a -> IsCubical (a .cont)

  Evidence of axis cubicality -> evidence of underlying container cubicality

Visibility: public export

dimHelper : IsCubical a -> Nat

  Extract the dimension from IsCubical with axis implicit

Visibility: public export

dim : (0 a : Axis) -> IsCubical a => Nat

  Extract the dimension from an axis which we know is cubical

Visibility: public export

dimsHelper : All IsCubical shape -> List Nat

  Extract the dimensions of cubical axes, with shape implicit

Visibility: public export

dims : (0 shape : Vect r Axis) -> All IsCubical shape => List Nat

  Extract the dimensions of cubical axes, with shape explicit

Visibility: public export

size : (0 shape : Vect r Axis) -> All IsCubical shape => Nat

  Product of all the dimensions of a cubical tensors, i.e. its size

Visibility: public export

data IsNaperian : Axis -> Type

  Follows the pattern of `IsNaperian` from `Base.Object.Definition`

Totality: total
Visibility: public export
Constructor: 

MkIsNaperian : (name : AxisName) -> (pos : Type) -> IsNaperian (name ~> Nap pos)

Hint: 

IsNaperian a -> IsNaperian (a .cont)

toContNaperian : IsNaperian a -> IsNaperian (a .cont)

  Evidence of axis being Naperian -> evidence of container being Naperian

Visibility: public export

LogHelper : IsNaperian a => Type

  Extract the position type from IsNaperian with axis implicit

Visibility: public export

Log : (0 a : Axis) -> IsNaperian a => Type

  Extract the position type from an axis which we know is Naperian

Visibility: public export

data IsConcrete : Axis -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsConcrete : (name : AxisName) -> IsConcrete c -> IsConcrete (name ~> c)

toContConcrete : IsConcrete a -> IsConcrete (a .cont)

Visibility: public export