From 802dfae493f883b9b019b98e86a34712f7d07fcd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 14 Feb 2023 21:16:20 +0100
Subject: [PATCH] slight simplify

---
 lib/Quox/Syntax/DimEq.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index b6c2686..c59f76f 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -75,13 +75,13 @@ C eqs     :<? d = C $ eqs :< d
 
 private %inline
 ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
-ifVar i p = map $ \q => if isYes $ q `decEq` B i then p else q
+ifVar i p = map $ \q => if q == B i then p else q
 
+-- (using decEq instead of (==) because of the proofs below)
 private %inline
 checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
-checkConst Zero Zero eqs = C eqs
-checkConst One  One  eqs = C eqs
-checkConst _    _    _   = ZeroIsOne
+checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
+
 
 export
 setConst : Var d -> DimConst -> DimEq' d -> DimEq d