Add operator form for unsafe indexing

src/Data/NumIdr/Array/Array.idr

@@ -243,6 +243,7 @@ array v = MkArray COrder (calcStrides COrder s) s (fromList $ collapse v)
 
 infixl 10 !!
 infixl 10 !?
+infixl 10 !#
 infixl 11 !!..
 infixl 11 !?..
 
@@ -395,6 +396,7 @@ export
 elements : Array {rk} s a -> Vect (product s) a
 elements (MkArray _ sts sh p) =
   let elems = map (flip index p . getLocation' sts) (getAllCoords' sh)
+  -- TODO: prove that the number of elements is `product s`
   in assert_total $ case toVect (product sh) elems of Just v => v
 
 

src/Data/NumIdr/Matrix.idr

@@ -101,12 +101,12 @@ getColumn c mat = rewrite sym (minusZeroRight m) in indexRange [All, One c] mat
 export
 diagonal' : Matrix m n a -> Vector (minimum m n) a
 diagonal' mat with (viewShape mat)
-  _ | Shape [m,n] = fromFunctionNB _ (\[i] => indexUnsafe [i,i] mat)
+  _ | Shape [m,n] = fromFunctionNB _ (\[i] => mat!#[i,i])
 
 export
 diagonal : Matrix' n a -> Vector n a
 diagonal mat with (viewShape mat)
-  _ | Shape [n,n] = fromFunctionNB [n] (\[i] => indexUnsafe [i,i] mat)
+  _ | Shape [n,n] = fromFunctionNB [n] (\[i] => mat!#[i,i])
 
 
 --------------------------------------------------------------------------------

src/Data/NumIdr/Vector.idr

@@ -121,6 +121,7 @@ export
 --------------------------------------------------------------------------------
 
 
+||| Construct a vector by pulling coordinates from another vector.
 export
 swizzle : Vect n (Fin m) -> Vector m a -> Vector n a
 swizzle p v = rewrite sym (lengthCorrect p)