Data.Array.All

Reexports

Definitions

data El : List a -> List a -> Type

Totality: total
Visibility: public export
Constructors:

ZEl : El as as

SEl : El as (v :: bs) -> El as bs

elToNat : El as bs -> Nat

Totality: total
Visibility: export

0 elLemma : (el : El as (v :: bs)) -> LT (elToNat el) (length as)

Totality: total
Visibility: export

record ArrAll : (a -> Type) -> List a -> Type

  An immutable heterogeneous array of size `n`.
  
  This has different performance characteristics than
  `Data.List.Quantifiers.All`: Lookup is `O(1)`, while
  prepending and appending is `O(n)`.

Totality: total
Visibility: export
Constructor: 

AA : AnyPtr -> ArrAll f as

Projection: 

.arr : ArrAll f as -> AnyPtr

0 HArr : List Type -> Type

Totality: total
Visibility: public export

Index : (as : List a) -> Fin (length as) -> a

Totality: total
Visibility: public export

elemToFin : Elem a as -> Fin (length as)

Totality: total
Visibility: export

0 ElemLemma : (el : Elem a as) -> a = Index as (elemToFin el)

Totality: total
Visibility: export

at : ArrAll f as -> (x : Fin (length as)) -> f (Index as x)

  Safely access a value in a heterogeneous array at the given position.

Totality: total
Visibility: export

elem : ArrAll f as -> (0 a : {a:1880}) -> Elem a as => f a

  Safely access a value in a heterogeneous array
  at the position of the given tag

Totality: total
Visibility: export

data MArrAll : Type -> (a -> Type) -> List a -> Type

  A mutable array.

Totality: total
Visibility: export
Constructor: 

MA : AnyPtr -> MArrAll s f as

0 MHArr : Type -> List Type -> Type

Totality: total
Visibility: public export

set : MArrAll s f as -> (x : Fin (length as)) -> f (Index as x) -> F1' s

  Safely write a value to a mutable heterogeneous array.

Totality: total
Visibility: export

setElem : MArrAll s f as -> f a -> Elem a as => F1' s

  Safely write a value to a mutable heterogeneous array.

Totality: total
Visibility: export

setEls : MArrAll s f as -> All f bs -> El as bs -> F1' s

  Safely write a value to a mutable heterogeneous array.

Totality: total
Visibility: export

get : MArrAll s f as -> (x : Fin (length as)) -> F1 s (f (Index as x))

  Safely read a value from a mutable array.
  
  This returns the values thus read with unrestricted quantity, paired
  with a new linear token of quantity one to be further used in the
  linear context.

Totality: total
Visibility: export

getElem : MArrAll s f as -> (0 a : {a:2239}) -> Elem a as => F1 s (f a)

Totality: total
Visibility: export

setElems : All f as -> All (\{arg:0} => Elem {arg:0} bs) as => MArrAll s f bs -> F1' s

Totality: total
Visibility: export

mall1 : All f as -> F1 s (MArrAll s f as)

  Fills a new mutable heterogeneous array bound to linear computation `s`.

Totality: total
Visibility: export

unsafeFreeze : MArrAll s f as -> F1 s (ArrAll f as)

Totality: total
Visibility: export

mall : Lift1 s m => All f as -> m (MArrAll s f as)

  Fills a new mutable heterogeneous array

Totality: total
Visibility: export

all : All f as -> ArrAll f as

  Creates a new immutable heterogeneous array

Totality: total
Visibility: export