From fe1f03b7cd7cfeb9992a968b5a5cbebe8fbe9b7d Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 14 Apr 2023 17:42:31 +0100
Subject: Define Thinnings.

---
 obs.ipkg              |  1 +
 src/Core/Thinning.idr | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+)
 create mode 100644 src/Core/Thinning.idr

diff --git a/obs.ipkg b/obs.ipkg
index c225c40..a5e5bb9 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -8,3 +8,4 @@ options = "--total"
 
 modules
   = Core.Term
+  , Core.Thinning
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
new file mode 100644
index 0000000..0067ac4
--- /dev/null
+++ b/src/Core/Thinning.idr
@@ -0,0 +1,55 @@
+module Core.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+data Thinner : Nat -> Nat -> Type where
+  IsBase : Thinner n (S n)
+  IsDrop : Thinner m n -> Thinner m (S n)
+  IsKeep : Thinner m n -> Thinner (S m) (S n)
+
+export
+data Thins : Nat -> Nat -> Type where
+  IsId : n `Thins` n
+  IsThinner : Thinner m n -> m `Thins` n
+
+%name Thinner thin
+%name Thins thin
+
+-- Constructors ----------------------------------------------------------------
+
+export
+id : (0 n : Nat) -> n `Thins` n
+id n = IsId
+
+export
+drop : m `Thins` n -> m `Thins` S n
+drop IsId = IsThinner IsBase
+drop (IsThinner thin) = IsThinner (IsDrop thin)
+
+export
+keep : m `Thins` n -> S m `Thins` S n
+keep IsId = IsId
+keep (IsThinner thin) = IsThinner (IsKeep thin)
+
+-- Non-Identity ----------------------------------------------------------------
+
+export
+data IsNotId : m `Thins` n -> Type where
+  ItIsThinner : IsNotId (IsThinner thin)
+
+%name IsNotId prf
+
+-- Views -----------------------------------------------------------------------
+
+public export
+data View : m `Thins` n -> Type where
+  Id : (0 n : Nat) -> View (id n)
+  Drop : (thin : m `Thins` n) -> View (drop thin)
+  Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
+
+export
+view : (thin : m `Thins` n) -> View thin
+view IsId = Id m
+view (IsThinner IsBase) = Drop (id _)
+view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
+view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
-- 
cgit v1.2.3