diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 14:50:55 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 14:50:55 +0100 |
| commit | 5a53c75f533f2ae758635e1989c4e7fb2b6469d5 (patch) | |
| tree | 09adf279aa9b29964a4330673b6f2c4152838f4b /src/Core/Reduction.idr | |
| parent | f0b34a9132f1d0606a80f7f84b0ee55c8c09d46e (diff) | |
Prove whnfs do not reduce.
Diffstat (limited to 'src/Core/Reduction.idr')
| -rw-r--r-- | src/Core/Reduction.idr | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 7516648..9015d14 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -3,6 +3,7 @@ module Core.Reduction import Core.Environment import Core.Declarative import Core.Term +import Core.Term.NormalForm import Core.Term.Substitution import Core.Term.Thinned import Core.Thinning @@ -131,3 +132,25 @@ termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubject export typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf + +-- Whnfs Do Not Reduce --------------------------------------------------------- + +export +whnfNoTermStep : Whnf t -> Not (TermStep env t u a) +whnfNoTermStep (Ntrl (App n)) (AppStep step tmWf) = whnfNoTermStep (Ntrl n) step +whnfNoTermStep (Ntrl (App n)) (PiBeta tyWf tmWf tmWf1) impossible +whnfNoTermStep n (ConvStep step tyConv) = whnfNoTermStep n step + +export +whnfNoTypeStep : Whnf a -> Not (TypeStep env a b) +whnfNoTypeStep = whnfNoTermStep + +export +whnfTypeRedStays : Whnf a -> TypeReduce env a b -> a = b +whnfTypeRedStays n (Refl tyWf) = Refl +whnfTypeRedStays n (Step step steps) = absurd (whnfNoTypeStep n step) + +export +whnfTermRedStays : Whnf t -> TermReduce env t u a -> t = u +whnfTermRedStays n (Refl tmWf) = Refl +whnfTermRedStays n (Step step steps) = absurd (whnfNoTermStep n step) |