Define Thinned terms.

This is to unify parts of Environment and Substition.

1 files changed, 28 insertions, 0 deletions

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 28e229d..e52545d 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -6,6 +6,8 @@ import Core.Thinning
 
 import Syntax.PreorderReasoning
 
+%prefix_record_projections off
+
 -- Definition ------------------------------------------------------------------
 
 public export
@@ -53,3 +55,29 @@ wknHomo (Abs n t) thin1 thin2 =
   ~~ wkn t (keep thin2 n . keep thin1 n)       ...(wknHomo t (keep thin1 n) (keep thin2 n))
   ~~ wkn t (keep (thin2 . thin1) n)            ...(cong (wkn t) $ compKeep thin2 thin1 n)
 wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+
+-- Thinned Terms ---------------------------------------------------------------
+
+public export
+record Thinned (sx : Context) where
+  constructor Over
+  {0 sy : Context}
+  term : Term sy
+  thin : sy `Thins` sx
+
+%name Thinned t, u, v
+
+public export
+expand : Thinned sx -> Term sx
+expand (term `Over` thin) = wkn term thin
+
+public export
+shift : Thinned sx -> sx `Thins` sy -> Thinned sy
+shift (term `Over` thin') thin = term `Over` thin . thin'
+
+export
+expandShift :
+  (t : Thinned sx) ->
+  (thin : sx `Thins` sy) ->
+  expand (shift t thin) = wkn (expand t) thin
+expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin