diff options
Diffstat (limited to 'src/Core/Reduction.idr')
| -rw-r--r-- | src/Core/Reduction.idr | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index b6e2eb0..7516648 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -119,3 +119,15 @@ termRedImpliesConv (Step step steps) = TransTm (termStepImpliesConv step) (termRedImpliesConv steps) + +-- Subject Typing -------------------------------------------------------------- + +export +termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a +termStepImpliesSubjectWf (AppStep step tmWf) = AppWf (termStepImpliesSubjectWf step) tmWf +termStepImpliesSubjectWf (PiBeta tyWf tmWf tmWf1) = AppWf (AbsWf tyWf tmWf) tmWf1 +termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubjectWf step) tyConv + +export +typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a +typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf |