From c86d2ee3e55d1d29b807adf9b74235ae8c0f6fd7 Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Sun, 17 Jul 2022 22:34:36 +0100 Subject: [PATCH] docstring --- src/Tensor.idr | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Tensor.idr b/src/Tensor.idr index d443db258..e45c9420d 100644 --- a/src/Tensor.idr +++ b/src/Tensor.idr @@ -236,9 +236,7 @@ namespace MultiSlice slice {shape=(_ :: _)} (DynamicIndex _ :: xs) = slice xs ||| Slice or index `Tensor` axes. Each axis can either be sliced or indexed (or unaltered), and -||| this can be done with either static (`Nat`) or dynamic (`Tensor [] U64`) indices. Static and -||| dynamic slicing are specified in different ways. Slices, indices, static and dynamic can be -||| mixed arbitrarily in any given call to `slice`. +||| this can be done with either static (`Nat`) or dynamic (`Tensor [] U64`) indices. ||| ||| **Static indices** |||