diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 14:39:38 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 14:39:38 +0100 |
| commit | f0b34a9132f1d0606a80f7f84b0ee55c8c09d46e (patch) | |
| tree | 9a7dfb6f22849f856e7f12cc18566636856733a7 /src/Core/Reduction.idr | |
| parent | ac4933e88f0bbc0e6522c9a0dad50fdd85ccaa84 (diff) | |
Prove subject typing.
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 |