diff options
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 |