diff options
| -rw-r--r-- | src/Core/Thinning.idr | 14 | ||||
| -rw-r--r-- | src/Core/Var.idr | 4 |
2 files changed, 9 insertions, 9 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index 5c380df..e70cf56 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -47,8 +47,8 @@ data View : sx `Thins` sy -> Type where Drop : (thin : sx `Thins` sy) -> (0 n : Name) -> View (drop thin n) Keep : (thin : sx `Thins` sy) -> + {auto 0 prf : IsNotId thin} -> -- For uniqueness (0 n : Name) -> - (0 prf : IsNotId thin) -> -- For uniqueness View (keep thin n) %name View view @@ -58,7 +58,7 @@ 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 ItIsThinner +view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n -- Operations ------------------------------------------------------------------ @@ -141,26 +141,26 @@ compAssoc' (Drop thin3 n) view2 view1 = Calc $ ~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) view2 view1) ~~ drop (thin3 . thin2) n . thin1 ..<(compLeftDrop (thin3 . thin2) thin1 n) ~~ (drop thin3 n . thin2) . thin1 ..<(cong (. thin1) $ compLeftDrop thin3 thin2 n) -compAssoc' (Keep thin3 n _) (Id _) view1 = cong (. thin1) $ sym $ compRightIdentity (keep thin3 n) -compAssoc' (Keep thin3 n _) (Drop thin2 n) view1 = Calc $ +compAssoc' (Keep thin3 n) (Id _) view1 = cong (. thin1) $ sym $ compRightIdentity (keep thin3 n) +compAssoc' (Keep thin3 n) (Drop thin2 n) view1 = Calc $ |~ keep thin3 n . (drop thin2 n . thin1) ~~ keep thin3 n . drop (thin2 . thin1) n ...(cong (keep thin3 n .) $ compLeftDrop thin2 thin1 n) ~~ drop (thin3 . (thin2 . thin1)) n ...(compRightDrop thin3 (thin2 . thin1) n) ~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) view1) ~~ drop (thin3 . thin2) n . thin1 ..<(compLeftDrop (thin3 . thin2) thin1 n) ~~ (keep thin3 n . drop thin2 n) . thin1 ..<(cong (. thin1) $ compRightDrop thin3 thin2 n) -compAssoc' (Keep thin3 n _) (Keep thin2 n _) (Id _) = Calc $ +compAssoc' (Keep thin3 n) (Keep thin2 n) (Id _) = Calc $ |~ keep thin3 n . (keep thin2 n . id _) ~~ keep thin3 n . keep thin2 n ...(cong (keep thin3 n .) $ compRightIdentity (keep thin2 n)) ~~ (keep thin3 n . keep thin2 n) . id _ ..<(compRightIdentity (keep thin3 n . keep thin2 n)) -compAssoc' (Keep thin3 n _) (Keep thin2 n _) (Drop thin1 n) = Calc $ +compAssoc' (Keep thin3 n) (Keep thin2 n) (Drop thin1 n) = Calc $ |~ keep thin3 n . (keep thin2 n . drop thin1 n) ~~ keep thin3 n . drop (thin2 . thin1) n ...(cong (keep thin3 n .) $ compRightDrop thin2 thin1 n) ~~ drop (thin3 . (thin2 . thin1)) n ...(compRightDrop thin3 (thin2 . thin1) n) ~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) (view thin1)) ~~ keep (thin3 . thin2) n . drop thin1 n ..<(compRightDrop (thin3 . thin2) thin1 n) ~~ (keep thin3 n . keep thin2 n) . drop thin1 n ..<(cong (. drop thin1 n) $ compKeep thin3 thin2 n) -compAssoc' (Keep thin3 n _) (Keep thin2 n _) (Keep thin1 n _) = Calc $ +compAssoc' (Keep thin3 n) (Keep thin2 n) (Keep thin1 n) = Calc $ |~ keep thin3 n . (keep thin2 n . keep thin1 n) ~~ keep thin3 n . keep (thin2 . thin1) n ...(cong (keep thin3 n .) $ compKeep thin2 thin1 n) ~~ keep (thin3 . (thin2 . thin1)) n ...(compKeep thin3 (thin2 . thin1) n) 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 |