From 8c00d98681c48d2e270aba00725a865307a653e1 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 31 Mar 2023 16:42:47 +0100 Subject: Make Views on thinnings unique. --- src/Core/Thinning.idr | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'src/Core/Thinning.idr') diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index 425d4ad..5781eaa 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -17,6 +17,10 @@ data Thins : Context -> Context -> Type where %name Thinner thinner %name Thins thin +export +data IsNotId : sx `Thins` sy -> Type where + ItIsThinner : IsNotId (IsThinner thinner) + -- Constructors ---------------------------------------------------------------- export @@ -39,11 +43,15 @@ public export data View : sx `Thins` sy -> Type where Id : (0 sx : Context) -> View (id sx) Drop : (thin : sx `Thins` sy) -> (0 n : Name) -> View (drop thin n) - Keep : (thin : sx `Thins` sy) -> (0 n : Name) -> View (keep thin n) + Keep : + (thin : sx `Thins` sy) -> + (0 n : Name) -> + (0 prf : IsNotId thin) -> -- For uniqueness + View (keep thin n) export view : (thin : sx `Thins` sy) -> View thin view IsId = Id sx view (IsThinner (IsBase n)) = Drop IsId n view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n -view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n +view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n ItIsThinner -- cgit v1.2.3