From 5be8f9d87c1a76cb9dcbf54b9c83b0e943f93c41 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 1 Apr 2023 13:37:25 +0100 Subject: Prove reduction subject typing. --- src/Core/Reduction.idr | 5 +++++ 1 file changed, 5 insertions(+) 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 --------------------------------------------------------- -- cgit v1.2.3