From d71ac8c34d70a42caa4cf3e1e34eb40ec6a99492 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 19 Feb 2023 17:02:13 +0100
Subject: [PATCH] rename Equal.Env to CmpContext

---
 lib/Quox/Equal.idr | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index fa704bb..77627a8 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -9,23 +9,23 @@ import Data.Maybe
 
 
 public export
-record Env where
-  constructor MakeEnv
+record CmpContext where
+  constructor MkCmpContext
   mode : EqMode
 
 
 public export
-0 HasEnv : (Type -> Type) -> Type
-HasEnv = MonadReader Env
+0 HasCmpContext : (Type -> Type) -> Type
+HasCmpContext = MonadReader CmpContext
 
 public export
 0 CanEqual : (q : Type) -> (Type -> Type) -> Type
-CanEqual q m = (HasErr q m, HasEnv m)
+CanEqual q m = (HasErr q m, HasCmpContext m)
 
 
 
 private %inline
-mode : HasEnv m => m EqMode
+mode : HasCmpContext m => m EqMode
 mode = asks mode
 
 private %inline
@@ -287,7 +287,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
       compare : (ty, s, t : Term q d n) -> m ()
       compare ty s t = do
         defs <- ask
-        runReaderT {m} (MakeEnv {mode}) $
+        runReaderT {m} (MkCmpContext {mode}) $
           for_ (splits ctx.dctx) $ \th =>
             compare0 defs (map (/// th) ctx.tctx)
                      (ty /// th) (s /// th) (t /// th)
@@ -296,7 +296,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
       compareType : (s, t : Term q d n) -> m ()
       compareType s t = do
         defs <- ask
-        runReaderT {m} (MakeEnv {mode}) $
+        runReaderT {m} (MkCmpContext {mode}) $
           for_ (splits ctx.dctx) $ \th =>
             compareType defs (map (/// th) ctx.tctx) (s /// th) (t /// th)
 
@@ -307,7 +307,7 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
       compare : (e, f : Elim q d n) -> m ()
       compare e f = do
         defs <- ask
-        runReaderT {m} (MakeEnv {mode}) $
+        runReaderT {m} (MkCmpContext {mode}) $
           for_ (splits ctx.dctx) $ \th =>
             compare0 defs (map (/// th) ctx.tctx) (e /// th) (f /// th)