diff options
| -rw-r--r-- | src/Core/Reduction.idr | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 21e6ee5..54a4523 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -50,9 +50,26 @@ namespace Term -- Reduction Subsumed by Conversion -------------------------------------------- termStepImpliesTermConv : TermStep env t u a -> TermConv env t u a +termStepImpliesTermConv (PiBeta wf wf1 wf2) = PiBeta wf wf1 wf2 +termStepImpliesTermConv (AppStep step wf) = AppConv (termStepImpliesTermConv step) (ReflTerm wf) +termStepImpliesTermConv (StepConv step conv) = ConvTermConv (termStepImpliesTermConv step) conv + typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b +typeStepImpliesTypeConv step = LiftConv (termStepImpliesTermConv step) + typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b +typeRedImpliesTypeConv (Stay wf) = ReflType wf +typeRedImpliesTypeConv (step :: steps) = + TransType + (typeStepImpliesTypeConv step) + (typeRedImpliesTypeConv steps) + termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a +termRedImpliesTermConv (Stay wf) = ReflTerm wf +termRedImpliesTermConv (step :: steps) = + TransTerm + (termStepImpliesTermConv step) + (termRedImpliesTermConv steps) -- Subject Typing -------------------------------------------------------------- |