From 325e128063216a51fd857945a0b7a70ff9bcc492 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 10 Feb 2024 11:39:07 +0100 Subject: [PATCH] =?UTF-8?q?add=20=CE=B7=20for=20False=20and=20True?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/Quox/Equal.idr | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 3ec9c0a..470fd2b 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -259,15 +259,16 @@ namespace Term compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t SOne => clashT loc ctx ty s t - compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $ + compare0' defs ctx sg ty@(Enum cases _) s t = local_ Equal $ + -- η for empty & singleton enums + if length (SortedSet.toList cases) <= 1 then pure () else case (s, t) of -- -------------------- - -- Γ ⊢ `t = `t ⇐ {ts} + -- Γ ⊢ 't = 't ⇐ {ts} -- -- t ∈ ts is in the typechecker, not here, ofc - (Tag t1 {}, Tag t2 {}) => - unless (t1 == t2) $ clashT s.loc ctx ty s t - (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f + (Tag t1 {}, Tag t2 {}) => unless (t1 == t2) $ clashT s.loc ctx ty s t + (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f (Tag {}, E _) => clashT s.loc ctx ty s t (E _, Tag {}) => clashT s.loc ctx ty s t