diff options
| -rw-r--r-- | src/Core/Reduction.idr | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 40829f3..b6e2eb0 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -91,3 +91,31 @@ export termRedRespEq : TermReduce env1 t u a -> env1 =~= env2 -> TermReduce env2 t u a termRedRespEq (Refl tmWf) prf = Refl (termWfRespEq tmWf prf) termRedRespEq (Step step steps) prf = Step (termStepRespEq step prf) (termRedRespEq steps prf) + +-- Reduction Subsumed by Conversion -------------------------------------------- + +export +termStepImpliesConv : TermStep env t u a -> TermConv env t u a +termStepImpliesConv (AppStep step tmWf) = AppConv (termStepImpliesConv step) (ReflTm tmWf) +termStepImpliesConv (PiBeta tyWf tmWf tmWf1) = PiBeta tyWf tmWf tmWf1 +termStepImpliesConv (ConvStep step tyConv) = ConvConv (termStepImpliesConv step) tyConv + +export +typeStepImpliesConv : TypeStep env a b -> TypeConv env a b +typeStepImpliesConv = LiftConv . termStepImpliesConv + +export +typeRedImpliesConv : TypeReduce env a b -> TypeConv env a b +typeRedImpliesConv (Refl tyWf) = ReflTy tyWf +typeRedImpliesConv (Step step steps) = + TransTy + (typeStepImpliesConv step) + (typeRedImpliesConv steps) + +export +termRedImpliesConv : TermReduce env t u a -> TermConv env t u a +termRedImpliesConv (Refl tmWf) = ReflTm tmWf +termRedImpliesConv (Step step steps) = + TransTm + (termStepImpliesConv step) + (termRedImpliesConv steps) |