From 762a41c32b520c11b06e1a1d35222e1c4fa4ac00 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Thu, 25 Apr 2024 13:38:22 -0400 Subject: [PATCH] Remove redundant `array'` function --- src/Data/NumIdr/Array/Array.idr | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index fb33630..deadcc8 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -171,22 +171,12 @@ fromFunction : {default B rep : Rep} -> RepConstraint rep a => (s : Vect rk Nat) -> (Coords s -> a) -> Array s a fromFunction s f = MkArray rep s (PrimArray.fromFunction s f) -||| Construct an array using a structure of nested vectors. The elements are arranged -||| to the specified order before being written. -||| -||| @ s The shape of the constructed array -||| @ ord The order of the constructed array -export -array' : {default B rep : Rep} -> RepConstraint rep a => - (s : Vect rk Nat) -> Vects s a -> Array s a -array' s v = MkArray rep s (fromVects s v) - ||| Construct an array using a structure of nested vectors. ||| To explicitly specify the shape and order of the array, use `array'`. export array : {default B rep : Rep} -> RepConstraint rep a => {s : Vect rk Nat} -> Vects s a -> Array s a -array {rep} = array' {rep} _ +array v = MkArray rep s (fromVects s v) --------------------------------------------------------------------------------