From bc3230e0007b4ddd2b4f07ddcc8629113a21e5b8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 01:28:49 +0100
Subject: [PATCH] rename Error.inj to one

---
 src/Quox/Error.idr | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index 2175057..477e8f5 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -36,8 +36,8 @@ Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
 
 
 export %inline
-inj : ty `Elem` tys => ty -> OneOf tys
-inj @{elem} value = One {elem, value}
+one : type `Elem` types => type -> OneOf types
+one @{elem} value = One {elem, value}
 
 ||| `All p types` computes a constraint for `p a` for each `a` in `types`
 public export
@@ -189,7 +189,7 @@ implementation
   (Monad m, err `Elem` errs) =>
   MonadThrow err (ErrorT errs m)
 where
-  throw = MkErrorT . pure . Left . inj
+  throw = MkErrorT . pure . Left . one
 
 export %inline
 implementation