From 5bcb0623a1b15aa2a46ab3a922c0f4b500d7d8e6 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 1 Apr 2023 14:46:40 +0100 Subject: Make the thinning View uniqueness proof implicit. Almost no users of the view use this proof. Hide the details from users. --- src/Core/Var.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Core/Var.idr') 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 -- cgit v1.2.3