Simple usage example

1 files changed, 5 insertions, 0 deletions

diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index 7d4621a..fa40921 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -425,12 +425,17 @@ data SShape sh where
   ShNil :: SShape '[]
   ShCons :: SNat n -> SShape sh -> SShape (n : sh)
 deriving instance Show (SShape sh)
+infixr 5 `ShCons`
 
 -- | A statically-known shape of a shape-typed array.
 class KnownShape sh where knownShape :: SShape sh
 instance KnownShape '[] where knownShape = ShNil
 instance (KnownNat n, KnownShape sh) => KnownShape (n : sh) where knownShape = ShCons knownNat knownShape
 
+sshapeKnown :: SShape sh -> Dict KnownShape sh
+sshapeKnown ShNil = Dict
+sshapeKnown (ShCons n sh) | Dict <- snatKnown n, Dict <- sshapeKnown sh = Dict
+
 lemKnownMapJust :: forall sh. KnownShape sh => Proxy sh -> Dict KnownShapeX (MapJust sh)
 lemKnownMapJust _ = X.lemKnownShapeX (go (knownShape @sh))
   where