diff options
Diffstat (limited to 'src/Data/Array/Mixed')
| -rw-r--r-- | src/Data/Array/Mixed/Lemmas.hs | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs index 7b3365b..7f41a06 100644 --- a/src/Data/Array/Mixed/Lemmas.hs +++ b/src/Data/Array/Mixed/Lemmas.hs @@ -56,20 +56,14 @@ lemRankApp :: forall sh1 sh2. -> Rank (sh1 ++ sh2) :~: Rank sh1 + Rank sh2 lemRankApp ZKX _ = Refl lemRankApp (_ :!% (ssh1 :: StaticShX sh1T)) ssh2 - = lem2 (Proxy @(Rank sh1T)) Proxy Proxy $ - lem (Proxy @(Rank sh2)) (Proxy @(Rank sh1T)) (Proxy @(Rank (sh1T ++ sh2))) $ - lemRankApp ssh1 ssh2 + = lem (Proxy @(Rank sh1T)) Proxy Proxy $ + sym (lemRankApp ssh1 ssh2) where lem :: proxy a -> proxy b -> proxy c - -> c :~: b + a - -> b + a :~: c + -> (a + b :~: c) + -> c + 1 :~: (a + 1 + b) lem _ _ _ Refl = Refl - lem2 :: proxy a -> proxy b -> proxy c - -> (a + b :~: c) - -> c + 1 :~: (a + 1 + b) - lem2 _ _ _ Refl = Refl - lemRankAppComm :: StaticShX sh1 -> StaticShX sh2 -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1) lemRankAppComm _ _ = unsafeCoerceRefl -- TODO improve this |