diff options
| -rw-r--r-- | src/Core/Reduction.idr | 10 |
1 files changed, 10 insertions, 0 deletions
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 -------------------------------------------------- |