Data.Linear.LVect(source)

Definitions

data LVect : Nat -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : LVect 0 a

(::) : a -@ (LVect n a -@ LVect (S n) a)

Hints:

Consumable a => Consumable (LVect n a)

Duplicable a => Duplicable (LVect n a)

lookup : Fin (S n) -@ (LVect (S n) a -@ LPair a (LVect n a))

Totality: total
Visibility: export

insertAt : Fin (S n) -@ (a -@ (LVect n a -@ LVect (S n) a))

Totality: total
Visibility: export

uncurry : (a -@ (b -@ c)) -@ (LPair a b -@ c)

Totality: total
Visibility: export

lookupInsertAtIdentity : (k : Fin (S n)) -> (vs : LVect (S n) a) -> uncurry (insertAt k) (lookup k vs) = vs

Totality: total
Visibility: export

insertAtLookupIdentity : (k : Fin (S n)) -> (w : a) -> (vs : LVect n a) -> lookup k (insertAt k w vs) = w # vs

Totality: total
Visibility: export

(<$>) : a -@ b -> LVect n a -@ LVect n b

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 4

pure : a -> LVect n a

Totality: total
Visibility: export

(<*>) : LVect n (a -@ b) -@ (LVect n a -@ LVect n b)

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 3

zip : LVect n a -@ (LVect n b -@ LVect n (LPair a b))

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 6

unzip : LVect n (LPair a b) -@ LPair (LVect n a) (LVect n b)

Totality: total
Visibility: export

splitAt : (1 m : Nat) -> LVect (m + n) a -@ LPair (LVect m a) (LVect n a)

Totality: total
Visibility: export

(++) : LVect m a -@ (LVect n a -@ LVect (m + n) a)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

lfoldr : (0 p : (Nat -> Type)) -> a -@ (p n -@ p (S n)) -> p 0 -@ (LVect n a -@ p n)

Totality: total
Visibility: export

lfoldl : (0 p : (Nat -> Type)) -> a -@ (p n -@ p (S n)) -> p 0 -@ (LVect n a -@ p n)

Totality: total
Visibility: export

reverse : LVect m a -@ LVect m a

Totality: total
Visibility: export

map : (0 f : a -@ b) -> {auto 1 _ : n `Copies` f} -> LVect n a -@ LVect n b

  Map a linear vector

Totality: total
Visibility: export

length : Consumable a => LVect n a -@ LNat

  Extract all

Totality: total
Visibility: export

foldl : (0 f : acc -@ (a -@ acc)) -> {auto 1 _ : n `Copies` f} -> acc -@ (LVect n a -@ acc)

  Fold a linear vector.

Totality: total
Visibility: export

replicate : (1 n : LNat) -> (0 v : a) -> {auto 1 _ : toNat n `Copies` v} -> LVect (toNat n) a

Totality: total
Visibility: export

(>>=) : LVect n a -@ ((0 f : a -@ LVect m b) -> LVect (n * m) b)

  Bind a linear vector.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 1

copiesToVect : (n `Copies` v) -@ LVect n a

  Extract all the copies into a vector of the same length as the number of copies.

Totality: total
Visibility: export