diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 13:39:47 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 13:39:47 +0100 |
| commit | 4a6e8819d3f65d67fa3114173d7358c87b89da18 (patch) | |
| tree | 1e957855209a9ac0e9293e01351c23180fbc1bde | |
| parent | 5be8f9d87c1a76cb9dcbf54b9c83b0e943f93c41 (diff) | |
Prove Whnfs do not reduce.
| -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 -------------------------------------------------- |