From e3e810024343f0262b452cd9825ac77c6c897c16 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 8 Apr 2023 14:56:31 +0100
Subject: Define substitution judgements.

This completes the core rules and semantics.
---
 obs.ipkg                              |  1 +
 src/Core/Declarative/Substitution.idr | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 src/Core/Declarative/Substitution.idr

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)
-- 
cgit v1.2.3