:< package:harpie

pattern (:<) :: Array a -> Array a -> Array a

harpie Harpie.Array

Convenience pattern for row extraction and consolidation at the beginning of an Array.

>>> (x:<xs) = array [4] [0..3]

>>> x
UnsafeArray [] [0]

>>> xs
UnsafeArray [3] [1,2,3]

>>> (x:<xs)
UnsafeArray [4] [0,1,2,3]

pattern (:<) :: forall s sh st a os ls ds . (KnownNats s, KnownNats sh, KnownNats st, True ~ Eval (InsertOk 0 st sh), s ~ Eval (IncAt 0 st), ds ~ '[0], sh ~ Eval (DeleteDims ds s), KnownNats ls, KnownNats os, Eval (SlicesOk ds os ls s) ~ True, os ~ Eval (Replicate (Eval (Rank ds)) 1), ls ~ Eval (GetLastPositions ds s), st ~ Eval (SetDims ds ls s)) => Array sh a -> Array st a -> Array s a

harpie Harpie.Fixed

Convenience pattern for row extraction and consolidation at the beginning of an Array.

>>> (x:<xs) = array @'[4] [0..3]

>>> toDynamic x
UnsafeArray [] [0]

>>> toDynamic xs
UnsafeArray [3] [1,2,3]

>>> toDynamic (x:<xs)
UnsafeArray [4] [0,1,2,3]