From f0b34a9132f1d0606a80f7f84b0ee55c8c09d46e Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sun, 16 Apr 2023 14:39:38 +0100 Subject: Prove subject typing. --- src/Core/Reduction.idr | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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 -- cgit v1.2.3