Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

Add basic vector functions to Util

Browse source
This commit is contained in:
Nathan McCarty 2025-01-06 14:03:38 -05:00
parent 5b91c3815c
commit 061c733688
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/Util.md
View file

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