From 9039055d9a994bde34e0c0bfedad1a72cd9c17a7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 3 Jul 2023 18:21:50 +0100
Subject: Add literals as primitive term.

---
 src/Term/Semantics.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Term/Semantics.idr')

diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index 2e61040..e8424f2 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -49,7 +49,7 @@ fullSem' (App (MakePair t u _)) = do
   t <- sem' t
   u <- sem' u
   pure (\ctx => t ctx (u ctx))
-fullSem' Zero = pure (const 0)
+fullSem' (Lit n) = pure (const n)
 fullSem' (Suc t) = do
   t <- fullSem' t
   pure (S . t)
-- 
cgit v1.2.3