From cedc6109895a53ce6ed667e0391b232bf5463387 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 15 Jun 2023 16:09:42 +0100
Subject: WIP : use smarter weakenings.

---
 src/Total/NormalForm.idr | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/Total/NormalForm.idr')

diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index a7aba57..c3f16cf 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -29,7 +29,8 @@ data Neutral' where
 
 data Normal' where
   Ntrl : Neutral' t -> Normal' t
-  Abs : Normal' t -> Normal' (Abs (MakeBound t thin))
+  Const : Normal' t -> Normal' (Const t)
+  Abs : Normal' t -> Normal' (Abs t)
   Zero : Normal' Zero
   Suc : Normal' t -> Normal' (Suc t)
 
@@ -119,7 +120,7 @@ recNf'' Zero thin n relU relV =
   backStepsRel relU [<?recZero]
 recNf'' (Suc t) thin n relU relV =
   let rec = recNf'' t thin (invSuc n) relU relV in
-  backStepsRel (snd relV id _ rec) [<?recSuc]
+  backStepsRel (snd relV Id _ rec) [<?recSuc]
 recNf'' t@Var thin n relU relV =
   let 0 neT = WrapNe {thin} Var in
   let nfU = escape relU in
-- 
cgit v1.2.3