diff options
Diffstat (limited to 'src')
| -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 --------------------------------------------------------- |