diff options
| -rw-r--r-- | src/Core/Thinning.idr | 12 |
1 files changed, 10 insertions, 2 deletions
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 |