diff options
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 |