diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 13:37:25 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 13:37:25 +0100 |
| commit | 5be8f9d87c1a76cb9dcbf54b9c83b0e943f93c41 (patch) | |
| tree | 321e7a34853755780d18d449e031c81ee6ac167c | |
| parent | bf2876fde9b8fdd4aae286b4e077a47df45916f7 (diff) | |
Prove reduction subject typing.
| -rw-r--r-- | src/Core/Reduction.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 54a4523..d68a82a 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -74,7 +74,12 @@ termRedImpliesTermConv (step :: steps) = -- Subject Typing -------------------------------------------------------------- termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a +termStepImpliesSubjectWf (PiBeta wf wf1 wf2) = AppTerm (AbsTerm wf wf1) wf2 +termStepImpliesSubjectWf (AppStep step wf) = AppTerm (termStepImpliesSubjectWf step) wf +termStepImpliesSubjectWf (StepConv step conv) = ConvTerm (termStepImpliesSubjectWf step) conv + typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a +typeStepImpliesSubjectWf step = LiftType (termStepImpliesSubjectWf step) -- Whnfs Do Not Reduce --------------------------------------------------------- |