1 files changed, 34 insertions, 0 deletions
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
new file mode 100644
index 0000000..0bc6dcf
--- /dev/null
+++ b/src/Core/Term/Thinned.idr
@@ -0,0 +1,34 @@
+module Core.Term.Thinned
+
+import Core.Term
+import Core.Thinning
+
+%prefix_record_projections off
+
+infix 4 =~=
+
+-- Definition ------------------------------------------------------------------
+
+public export
+record Thinned (n : Nat) where
+  constructor Over
+  {0 m : Nat}
+  term : Term m
+  thin : m `Thins` n
+
+%name Thinned t, u, v
+
+%inline
+public export
+expand : Thinned n -> Term n
+expand (term `Over` thin) = wkn term thin
+
+public export
+(=~=) : Thinned n -> Thinned n -> Type
+t =~= u = expand t = expand u
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wkn : Thinned m -> m `Thins` n -> Thinned n
+wkn t thin = { thin $= (thin .) } t