Idris2Doc : Data.Tensor.Shape.Axis

Data.Tensor.Shape.Axis

(source)
Definitions
AxisName : Type
  The name for an axis is an arbitrary string

  Totality: total
  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
  Totality: total
  Visibility: public export
name : Axis -> AxisName
  Totality: total
  Visibility: public export
.cont : Axis -> Cont
  Totality: total
  Visibility: public export
cont : Axis -> Cont
  Totality: total
  Visibility: public export
rename : Axis -> AxisName -> Axis
  Totality: total
  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

  Totality: total
  Visibility: public export
At : (ax : Axis) -> (ax .cont) .Shp -> Axis
  Variant of container `At` for axes

  Totality: total
  Visibility: public export
(~~>) : AxisName -> Nat -> Axis
  A "constructor" for cubical axes

  Totality: total
  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

  Totality: total
  Visibility: public export
dimHelper : IsCubical a -> Nat
  Extract the dimension from IsCubical with axis implicit

  Totality: total
  Visibility: public export
.dim : (0 a : Axis) -> IsCubical a => Nat
  Extract the dimension from an axis which we know is cubical

  Totality: total
  Visibility: public export
dimsHelper : All IsCubical shape -> List Nat
  Extract the dimensions of cubical axes, with shape implicit

  Totality: total
  Visibility: public export
dims : (0 shape : Vect r Axis) -> All IsCubical shape => List Nat
  Extract the dimensions of cubical axes, with shape explicit

  Totality: total
  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

  Totality: total
  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

  Totality: total
  Visibility: public export
LogHelper : IsNaperian a => Type
  Extract the position type from IsNaperian with axis implicit

  Totality: total
  Visibility: public export
Log : (0 a : Axis) -> IsNaperian a => Type
  Extract the position type from an axis which we know is Naperian

  Totality: total
  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)
  Totality: total
  Visibility: public export