From fe25edfd8e633a834a23d272bae8ccf456b63c26 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Thu, 9 Apr 2026 00:59:15 +0200 Subject: Make equal-rank-coercibility part of the interface of ListX --- src/Data/Array/Nested/Lemmas.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/Data/Array/Nested/Lemmas.hs') 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 -- cgit v1.3