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 + 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) +``` +