From 863849e4c459321b29631e5f82d7add2f12eb5b0 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 13 May 2024 01:23:14 +0200 Subject: [PATCH] =?UTF-8?q?clean=20up=20subsing=20=CE=B7=20stuff?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/Quox/Equal.idr | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 5998b3d..5ac02b2 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -278,13 +278,9 @@ namespace Term eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () eta loc e (S _ (N b)) = - if qty /= One then - if !(isSubSing defs ctx sg arg) then - compare0 defs ctx' sg res.term (toLamBody e) (weakT 1 b) - else - clashT loc ctx ty s t - else - clashT loc ctx ty s t + if !(pure (qty /= One) `andM` isSubSing defs ctx sg arg) + then compare0 defs ctx' sg res.term (toLamBody e) (weakT 1 b) + else clashT loc ctx ty s t eta _ e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b