diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-31 16:42:47 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-31 16:42:47 +0100 |
| commit | 8c00d98681c48d2e270aba00725a865307a653e1 (patch) | |
| tree | 0fc4d015a6f286f72dd06016827b38da6a1dd045 /src | |
| parent | e2d4e40ae7c86395dc34f9894c10169c20517615 (diff) | |
Make Views on thinnings unique.
Diffstat (limited to 'src')
| -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 |