From 47069a9316cccb3b44dda5d4e6339c0aa7c20fa8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 24 Nov 2023 17:23:45 +0100
Subject: [PATCH] fill a stray hole

---
 lib/Quox/Whnf/Main.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 2c0a67a..75a1248 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -255,7 +255,7 @@ CanWhnf Term Interface.isRedexT where
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
-      Right nc => pure $ Element (Succ p loc) nc
+      Right nc => pure $ nred $ Succ p loc
 
   whnf defs ctx sg (Let _ rhs body _) =
     whnf defs ctx sg $ sub1 body rhs