diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 14:35:26 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 14:35:26 +0100 |
| commit | ac4933e88f0bbc0e6522c9a0dad50fdd85ccaa84 (patch) | |
| tree | 6d4a914d3ab3be273a013b6715845a7eb8895d60 /src/Core/Reduction.idr | |
| parent | cdcfdcd31ccfee2b2a491713b4527ca87dd586bf (diff) | |
Prove conversion subsumes reduction.
Diffstat (limited to 'src/Core/Reduction.idr')
| -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) |