idris-matrix

A simple Idris library for manipulating matrices 🧙

commit 1add772cdb3949a50f0b23b9e290393382c6ddcf
parent f6bba90fa473bb141cd484552520c28d4eacde84
Author: Pablo <pablo-escobar@riseup.net>
Date:   Sat,  1 May 2021 19:31:15 +0000

Converted the README to Markdown

Diffstat:
MData/Matrix.idr | 8++++----
DREADME.adoc | 6------
AREADME.md | 6++++++
3 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/Data/Matrix.idr b/Data/Matrix.idr
@@ -125,16 +125,16 @@ export total
     f : Num t => Fin (S n) -> Fin (S p) -> t
     f i j = sum (zipWith (*) (with Vect index i as) (with Vect index j bs'))
 
-infixr 8 <>
+infixr 8 .
 
 ||| Multiplies a matrix by a scalar.
 export total
-(<>) : Num t => t -> Matrix (S n) (S m) t -> Matrix (S n) (S m) t
-x <> as = (x *) <$> as
+(.) : Num t => t -> Matrix (S n) (S m) t -> Matrix (S n) (S m) t
+x . as = (x *) <$> as
 
 export total
 negate : Neg t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t
-negate as = negate <$> as
+negate = negate <$>
 
 export total
 (-) : Neg t => Matrix (S n) (S m) t -> Matrix (S n) (S m) t 
diff --git a/README.adoc b/README.adoc
@@ -1,6 +0,0 @@
-= Data.Matrix
-
-A simple Idris library for manipulating matrices 🧙
-
-This is mostly an exercise.
-
diff --git a/README.md b/README.md
@@ -0,0 +1,6 @@
+## Data.Matrix
+
+A simple Idris library for manipulating matrices 🧙
+
+This is mostly an exercise.
+