Data.Container.Base.Extension.Definition

Definitions

record Ext : (0 _ : Cont) -> Type -> Type

  Extension of a container
  This allows us to talk about the content, or payload of a container

Totality: total
Visibility: public export
Constructor: 

(<|) : (shapeExt : c .Shp) -> (c .Pos shapeExt -> x) -> Ext c x

Projections:

.index : ({rec:0} : Ext c x) -> c .Pos (shapeExt {rec:0}) -> x

.shapeExt : Ext c x -> c .Shp

Hints:

ProdMonoid c => Alternative (Ext c)

TensorMonoid c => Applicative (Ext c)

IsNaperian c => Applicative (Ext c)

Functor (Ext c)

Functor (Ext d . Ext c)

SeqMonoid c => Monad (Ext c)

.shapeExt : Ext c x -> c .Shp

Visibility: public export

shapeExt : Ext c x -> c .Shp

Visibility: public export

.index : ({rec:0} : Ext c x) -> c .Pos (shapeExt {rec:0}) -> x

Visibility: public export

index : ({rec:0} : Ext c x) -> c .Pos (shapeExt {rec:0}) -> x

Visibility: public export

fullOf : Cont -> Type -> Type

  In `Ext c x`, the container `c` is said to be "full off" values of type `x`
  `fullOf` is sometimes used as infix operator to aid readability

Visibility: public export

Path : Cont -> Type

Visibility: public export

set : InterfaceOnPositions c Eq => (e : Ext c x) -> c .Pos (shapeExt e) -> x -> Ext c x

  The `index` field of an extension defines a "getter" for a container
  This is the container setter

Visibility: public export

mapShapeExt : (l : fullOf c a) -> shapeExt (f <$> l) = shapeExt l

  Map ing over an extension preserves its shape 

Visibility: public export

mapIndexCont : (l : fullOf c a) -> (ps : c .Pos (shapeExt (f <$> l))) -> f (index l (rewrite__impl {_:17090} {_:17089} ps)) = index (f <$> l) ps

  Indexing over a mapped extension is the same as indexing over a rewrite
  of the map

Visibility: public export

record EqExt : Ext c a -> Ext c a -> Type

  Structure needed to store equality data for Ext.
  To prove that two extensions `e1, e2` are equal, we need to provide a proof
  in two steps, and use the first one to rewrite the second. That is, we need
  a) a proof that the chosen shape types are equal. This allows us to 
  rewrite the position maps of both extensions to the same type.
  b) for each shape, a proof that the positions are equal as types

Totality: total
Visibility: public export
Constructor: 

MkEqExt : (shapesEqual : e1 .shapeExt = e2 .shapeExt) -> ((p : c .Pos (e1 .shapeExt)) -> e1 .index p = e2 .index (rewrite__impl (c .Pos) (sym shapesEqual) p)) -> EqExt e1 e2

Projections:

.shapesEqual : EqExt e1 e2 -> e1 .shapeExt = e2 .shapeExt

  The shapes must be equal

.valuesEqual : ({rec:0} : EqExt e1 e2) -> (p : c .Pos (e1 .shapeExt)) -> e1 .index p = e2 .index (rewrite__impl (c .Pos) (sym (shapesEqual {rec:0})) p)

  For each position in that shape, the values must be equal
  Relying on rewrite to get the correct type for the position

.shapesEqual : EqExt e1 e2 -> e1 .shapeExt = e2 .shapeExt

  The shapes must be equal

Visibility: public export

shapesEqual : EqExt e1 e2 -> e1 .shapeExt = e2 .shapeExt

  The shapes must be equal

Visibility: public export

.valuesEqual : ({rec:0} : EqExt e1 e2) -> (p : c .Pos (e1 .shapeExt)) -> e1 .index p = e2 .index (rewrite__impl (c .Pos) (sym (shapesEqual {rec:0})) p)

  For each position in that shape, the values must be equal
  Relying on rewrite to get the correct type for the position

Visibility: public export

valuesEqual : ({rec:0} : EqExt e1 e2) -> (p : c .Pos (e1 .shapeExt)) -> e1 .index p = e2 .index (rewrite__impl (c .Pos) (sym (shapesEqual {rec:0})) p)

  For each position in that shape, the values must be equal
  Relying on rewrite to get the correct type for the position

Visibility: public export

decEqExt : (e1 : Ext c a) -> (e2 : Ext c a) -> EqExt e1 e2 -> Dec (e1 = e2)

  Another alternative is to use DecEq, and a different explicit rewrite