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