From 4a6e8819d3f65d67fa3114173d7358c87b89da18 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:39:47 +0100
Subject: Prove Whnfs do not reduce.

---
 src/Core/Reduction.idr | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src')

diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index d68a82a..5a9622e 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -86,12 +86,22 @@ typeStepImpliesSubjectWf step = LiftType (termStepImpliesSubjectWf step)
 -- Cannot step from whnf
 
 termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
+termStepWhnfImpossible n (StepConv step conv) = termStepWhnfImpossible n step
+termStepWhnfImpossible (Ntrl (App n)) (PiBeta wf wf1 wf2) impossible
+termStepWhnfImpossible (Ntrl (App n)) (AppStep step wf) = termStepWhnfImpossible (Ntrl n) step
+
 typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)
+typeStepWhnfImpossible = termStepWhnfImpossible
 
 -- Reduction starting from whnf goes nowhere
 
 typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
+typeRedWhnfStays n (Stay wf) = Refl
+typeRedWhnfStays n (step :: steps) = absurd $ typeStepWhnfImpossible n step
+
 termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u
+termRedWhnfStays n (Stay wf) = Refl
+termRedWhnfStays n (step :: steps) = absurd $ termStepWhnfImpossible n step
 
 -- Reduction is Deterministic --------------------------------------------------
 
-- 
cgit v1.2.3