From 26b8f3c19cd919f5a45ef07e4ba76bae5cab35ce Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 16 May 2025 11:54:41 +0200
Subject: Shape/index function rename

---
 src/Data/Array/Mixed/Lemmas.hs | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

(limited to 'src/Data/Array/Mixed')

diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
index 7f41a06..cfb7bc6 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -64,16 +64,12 @@ lemRankApp (_ :!% (ssh1 :: StaticShX sh1T)) ssh2
         -> c + 1 :~: (a + 1 + b)
     lem _ _ _ Refl = Refl
 
-lemRankAppComm :: StaticShX sh1 -> StaticShX sh2
+lemRankAppComm :: proxy sh1 -> proxy sh2
                -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
-lemRankAppComm _ _ = unsafeCoerceRefl  -- TODO improve this
-
-lemRankReplicate :: SNat n -> Rank (Replicate n (Nothing @Nat)) :~: n
-lemRankReplicate SZ = Refl
-lemRankReplicate (SS (n :: SNat nm1))
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @nm1
-  , Refl <- lemRankReplicate n
-  = Refl
+lemRankAppComm _ _ = unsafeCoerceRefl
+
+lemRankReplicate :: proxy n -> Rank (Replicate n (Nothing @Nat)) :~: n
+lemRankReplicate _ = unsafeCoerceRefl
 
 
 -- ** Various type families
-- 
cgit v1.2.3-70-g09d2