diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Core/Declarative/Substitution.idr | 28 |
2 files changed, 29 insertions, 0 deletions
@@ -9,6 +9,7 @@ options = "--total" modules = Core.Context , Core.Declarative + , Core.Declarative.Substitution , Core.Environment , Core.Name , Core.Reduction diff --git a/src/Core/Declarative/Substitution.idr b/src/Core/Declarative/Substitution.idr new file mode 100644 index 0000000..bd37432 --- /dev/null +++ b/src/Core/Declarative/Substitution.idr @@ -0,0 +1,28 @@ +module Core.Declarative.Substitution + +import Core.Context +import Core.Declarative +import Core.Environment +import Core.Thinning +import Core.Term +import Core.Term.Substitution + +-- Definition ------------------------------------------------------------------ + +public export +data SubstWf : Env sy -> Subst sx sy -> Env sx -> Type where + Base : IsExtension thin env2 env1 -> SubstWf env2 (Base thin) env1 + (:<) : + SubstWf env2 sub env1 -> + TermWf env2 (expand t) (expand a) -> + SubstWf env2 (sub :< t) (Add env1 a) + +namespace Conv + public export + data SubstConv : Env sy -> Subst sx sy -> Subst sx sy -> Env sx -> Type where + Base : IsExtension thin env2 env1 -> SubstConv env2 (Base thin) (Base thin) env1 + (:<) : + forall sub1, sub2. + SubstConv env2 sub1 sub2 env1 -> + TermConv env2 (expand t) (expand u) (expand a) -> + SubstConv env2 (sub1 :< t) (sub2 :< u) (Add env1 a) |