diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2026-04-09 00:59:15 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-09 18:39:54 +0200 |
| commit | 2e29470184d9b64b91d2709b7ac1f97f6c797886 (patch) | |
| tree | c8ea9b71575022cfc77569857aab7fb4306f20e6 /src/Data/Array/Nested/Lemmas.hs | |
| parent | 27f5fd474a85bd0c404215a1ce38ed378594e54b (diff) | |
Make equal-rank-coercibility part of the interface of ListX
Diffstat (limited to 'src/Data/Array/Nested/Lemmas.hs')
| -rw-r--r-- | src/Data/Array/Nested/Lemmas.hs | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Data/Array/Nested/Lemmas.hs b/src/Data/Array/Nested/Lemmas.hs index e61b148..43cab3e 100644 --- a/src/Data/Array/Nested/Lemmas.hs +++ b/src/Data/Array/Nested/Lemmas.hs @@ -146,9 +146,8 @@ lemRankAppComm _ _ = unsafeCoerceRefl lemRankReplicate :: proxy n -> Rank (Replicate n (Nothing @Nat)) :~: n lemRankReplicate _ = unsafeCoerceRefl -lemRankMapJust :: ShS sh -> Rank (MapJust sh) :~: Rank sh -lemRankMapJust ZSS = Refl -lemRankMapJust (_ :$$ sh') | Refl <- lemRankMapJust sh' = Refl +lemRankMapJust :: proxy sh -> Rank (MapJust sh) :~: Rank sh +lemRankMapJust _ = unsafeCoerceRefl -- ** Related to MapJust and/or Permutation |