diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-15 16:09:42 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-15 16:09:42 +0100 |
| commit | cedc6109895a53ce6ed667e0391b232bf5463387 (patch) | |
| tree | cb600a2b91255586821d94dba5137a8cb746c90e /src/Total/NormalForm.idr | |
| parent | f910e142ce7c10f8244ecfa40e41756fb8c8a53f (diff) | |
WIP : use smarter weakenings.better-thinning
Diffstat (limited to 'src/Total/NormalForm.idr')
| -rw-r--r-- | src/Total/NormalForm.idr | 5 |
1 files changed, 3 insertions, 2 deletions
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 |