diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-09 18:04:58 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-09 18:39:57 +0200 |
| commit | bcf3bcf63626e75af9ab316d988e146f9a60c81d (patch) | |
| tree | 956c3d5fd9a27974079fb8f3d5267df470656f25 /src/Data/Array/Nested/Lemmas.hs | |
| parent | 2e29470184d9b64b91d2709b7ac1f97f6c797886 (diff) | |
Follow up the equal-rank-coercibility introduction
Diffstat (limited to 'src/Data/Array/Nested/Lemmas.hs')
| -rw-r--r-- | src/Data/Array/Nested/Lemmas.hs | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Data/Array/Nested/Lemmas.hs b/src/Data/Array/Nested/Lemmas.hs index 43cab3e..850f8ea 100644 --- a/src/Data/Array/Nested/Lemmas.hs +++ b/src/Data/Array/Nested/Lemmas.hs @@ -6,7 +6,11 @@ {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} -module Data.Array.Nested.Lemmas where +module Data.Array.Nested.Lemmas ( + module Data.Array.Nested.Lemmas, + lemReplicateSucc, lemMapJustEmpty, lemMapJustCons, lemMapJustHead, + lemRankMapJust +) where import Data.Proxy import Data.Type.Equality @@ -146,9 +150,6 @@ lemRankAppComm _ _ = unsafeCoerceRefl lemRankReplicate :: proxy n -> Rank (Replicate n (Nothing @Nat)) :~: n lemRankReplicate _ = unsafeCoerceRefl -lemRankMapJust :: proxy sh -> Rank (MapJust sh) :~: Rank sh -lemRankMapJust _ = unsafeCoerceRefl - -- ** Related to MapJust and/or Permutation lemTakeLenMapJust :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh) |