diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:46:40 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:56:38 +0100 |
| commit | 5bcb0623a1b15aa2a46ab3a922c0f4b500d7d8e6 (patch) | |
| tree | 57b9e9f7a228d3228c6fa96aaa79f64f0b4cddf0 /src/Core/Var.idr | |
| parent | 296aa178fa3012f217cab1806dc70be0a1d2b6fc (diff) | |
Make the thinning View uniqueness proof implicit.
Almost no users of the view use this proof. Hide the details from users.
Diffstat (limited to 'src/Core/Var.idr')
| -rw-r--r-- | src/Core/Var.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Core/Var.idr b/src/Core/Var.idr index a16b47e..4e357aa 100644 --- a/src/Core/Var.idr +++ b/src/Core/Var.idr @@ -50,8 +50,8 @@ view (MakeVar (S k) (There prf)) = There (MakeVar k prf) doWkn : Var sx -> {0 thin : sx `Thins` sy} -> View thin -> Var sy doWkn i (Id sy) = i doWkn i (Drop thin n) = there $ doWkn i (view thin) -doWkn (MakeVar 0 Here) (Keep thin n _) = here -doWkn (MakeVar (S k) (There prf)) (Keep thin n _) = there $ doWkn (MakeVar k prf) (view thin) +doWkn (MakeVar 0 Here) (Keep thin n) = here +doWkn (MakeVar (S k) (There prf)) (Keep thin n) = there $ doWkn (MakeVar k prf) (view thin) export wkn : Var sx -> sx `Thins` sy -> Var sy |