From 8839dd049acd4f249e77d3bfe6e29db46146535f Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 16 Sep 2022 12:39:47 -0400 Subject: [PATCH] Add name suggestions to types --- src/Data/NumIdr/Array/Array.idr | 2 ++ src/Data/NumIdr/Matrix.idr | 4 +++- src/Data/NumIdr/Transform/Point.idr | 4 +++- src/Data/NumIdr/Transform/Translation.idr | 2 +- src/Data/NumIdr/Vector.idr | 1 + 5 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr index 9294ce8..c17d08d 100644 --- a/src/Data/NumIdr/Array/Array.idr +++ b/src/Data/NumIdr/Array/Array.idr @@ -43,6 +43,8 @@ data Array : (s : Vect rk Nat) -> (a : Type) -> Type where MkArray : (ord : Order) -> (sts : Vect rk Nat) -> (s : Vect rk Nat) -> PrimArray a -> Array s a +%name Array arr + -------------------------------------------------------------------------------- -- Properties of arrays diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index a4ca435..277d7a7 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -15,6 +15,8 @@ public export Matrix : Nat -> Nat -> Type -> Type Matrix m n = Array [m,n] +%name Matrix mat + ||| A synonym for a square matrix with dimensions of length `n`. public export Matrix' : Nat -> Type -> Type @@ -477,7 +479,7 @@ decompLUP {m,n} mat with (viewShape mat) -------------------------------------------------------------------------------- --- Matrix properties +-- Determinant -------------------------------------------------------------------------------- diff --git a/src/Data/NumIdr/Transform/Point.idr b/src/Data/NumIdr/Transform/Point.idr index 4f5b0f4..fdb9f06 100644 --- a/src/Data/NumIdr/Transform/Point.idr +++ b/src/Data/NumIdr/Transform/Point.idr @@ -5,7 +5,7 @@ import Data.NumIdr.PrimArray import Data.NumIdr.Array import Data.NumIdr.Vector import Data.NumIdr.Matrix -import Data.NumIdr.Multiply +import Data.NumIdr.Interfaces %default total @@ -15,6 +15,8 @@ record Point n a where constructor MkPoint vec : Vector n a +%name Point p,q,r + -------------------------------------------------------------------------------- -- Point constructors diff --git a/src/Data/NumIdr/Transform/Translation.idr b/src/Data/NumIdr/Transform/Translation.idr index 5c7c1dd..3cb8404 100644 --- a/src/Data/NumIdr/Transform/Translation.idr +++ b/src/Data/NumIdr/Transform/Translation.idr @@ -1,7 +1,7 @@ module Data.NumIdr.Transform.Translation import Data.Vect -import Data.NumIdr.Multiply +import Data.NumIdr.Interfaces import Data.NumIdr.Array import Data.NumIdr.Vector import Data.NumIdr.Transform.Point diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr index 37ddc69..41c8cfb 100644 --- a/src/Data/NumIdr/Vector.idr +++ b/src/Data/NumIdr/Vector.idr @@ -13,6 +13,7 @@ public export Vector : Nat -> Type -> Type Vector n = Array [n] +%name Vector v,w,u ||| The length (number of dimensions) of the vector. public export