diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-05-16 11:54:41 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-05-16 11:54:41 +0200 |
| commit | 26b8f3c19cd919f5a45ef07e4ba76bae5cab35ce (patch) | |
| tree | 8c17db3c627b10807c2f19ba8cc0c83ec551c69e /src/Data/Array/Mixed/Lemmas.hs | |
| parent | 09041ca155485885a2f337f71b04442e991a550d (diff) | |
Shape/index function rename
Diffstat (limited to 'src/Data/Array/Mixed/Lemmas.hs')
| -rw-r--r-- | src/Data/Array/Mixed/Lemmas.hs | 14 |
1 files changed, 5 insertions, 9 deletions
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 |