Define substitution judgements.

This completes the core rules and semantics.

2 files changed, 29 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index b6906d5..73ffaf9 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -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)