From ecd3be8bda8a57a87c298b5b2747e0613b85637c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 13 Mar 2023 19:39:29 +0100
Subject: [PATCH] =?UTF-8?q?"WhnfErr"=20=E2=87=92=20"WhnfError"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Quox/Reduce.idr   | 10 ++++------
 lib/Quox/Typing.idr   |  4 ++--
 tests/TypingImpls.idr |  4 ++--
 3 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 03ba095..80e8fde 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -13,7 +13,7 @@ import Data.List
 ||| errors that might happen if you pass an ill typed expression into
 ||| whnf. don't do that please
 public export
-data WhnfErr = MissingEnumArm TagVal (List TagVal)
+data WhnfError = MissingEnumArm TagVal (List TagVal)
 
 
 public export
@@ -21,9 +21,7 @@ public export
 RedexTest tm = forall q, d, n, g. Definitions' q g -> tm q d n -> Bool
 
 public export
-interface Whnf (0 tm : TermLike)
-               (0 isRedex : RedexTest tm)
-               (0 err : Type) | tm
+interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) (0 err : Type) | tm
 where
   whnf : (defs : Definitions' q g) ->
          tm q d n -> Either err (Subset (tm q d n) (No . isRedex defs))
@@ -107,7 +105,7 @@ mutual
 
 mutual
   export covering
-  Whnf Elim Reduce.isRedexE WhnfErr where
+  Whnf Elim Reduce.isRedexE WhnfError where
     whnf defs (F x) with (lookupElim x defs) proof eq
       _ | Just y  = whnf defs y
       _ | Nothing = pure $ Element (F x) $ rewrite eq in Ah
@@ -173,7 +171,7 @@ mutual
     whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el
 
   export covering
-  Whnf Term Reduce.isRedexT WhnfErr where
+  Whnf Term Reduce.isRedexT WhnfError where
     whnf _ t@(TYPE {}) = pure $ nred t
     whnf _ t@(Pi   {}) = pure $ nred t
     whnf _ t@(Lam  {}) = pure $ nred t
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 569a861..bfc726c 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -152,7 +152,7 @@ data Error q
     (Elim q d n) (Elim q d n)
     (Error q)
 
-| WhnfError WhnfErr
+| WhnfError WhnfError
 
 
 public export
@@ -215,7 +215,7 @@ substCasePairRet dty retty =
 
 parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   export covering %inline
-  whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfErr =>
+  whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
           tm q d n -> m (NonRedex tm q d n defs)
   whnfT = either (throwError . WhnfError) pure . whnf defs
 
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index 584bd82..c7915ed 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -9,7 +9,7 @@ import Derive.Prelude
 %language ElabReflection
 
 
-%runElab derive "WhnfErr" [Show]
+%runElab derive "Reduce.WhnfError" [Show]
 
 %runElab deriveIndexed "DimEq" [Show]
 
@@ -22,7 +22,7 @@ showTypingError : (PrettyHL q, Show q) => Show (Error q)
 showTypingError = deriveShow
 
 export
-ToInfo WhnfErr where
+ToInfo WhnfError where
   toInfo (MissingEnumArm t ts) =
     [("type", "MissingEnumArm"),
      ("tag", show t),