From 061c7336886f718c715e71f8989e42a4153db303 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 6 Jan 2025 14:03:38 -0500
Subject: [PATCH] Add basic vector functions to Util

---
 src/Util.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/Util.md b/src/Util.md
index 5e4db45..c551eea 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -22,3 +22,26 @@ Applies a function to the contents of a `Left` if the value of the given `Either
   mapLeft f (Left x) = Left (f x)
   mapLeft f (Right x) = Right x
 ```
+## Vectors
+
+Define some operations for pairs of numbers, treating them roughly like vectors
+
+### Addition and Subtraction
+
+<!-- idris
+export infixl 8 >+<
+export infixl 8 >-<
+
+namespace Pair
+-->
+
+```idris
+  public export
+  (>+<) : Num a => (x, y : (a, a)) -> (a, a)
+  (x_1, x_2) >+< (y_1, y_2) = (x_1 + y_1, x_2 + y_2)
+
+  public export
+  (>-<) : Neg a => (x, y : (a, a)) -> (a, a)
+  (x_1, x_2) >-< (y_1, y_2) = (x_1 - y_1, x_2 - y_2)
+```
+