Simple usage example

2 files changed, 22 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
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index 5dacc8a..b154f67 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -44,6 +44,10 @@ unSNat :: SNat n -> Natural
 unSNat SZ = 0
 unSNat (SS n) = 1 + unSNat n
 
+-- | Convert an 'SNat' to an integer.
+unSNat' :: SNat n -> Int
+unSNat' = fromIntegral . unSNat
+
 -- | A 'KnownNat' dictionary is just a singleton natural, so we can create
 -- evidence of 'KnownNat' given an 'SNat'.
 snatKnown :: SNat n -> Dict KnownNat n
@@ -68,3 +72,16 @@ gknownNat (Proxy @n) = go (knownNat @n)
     go :: SNat m -> Dict G.KnownNat (GNat m)
     go SZ = Dict
     go (SS n) | Dict <- go n = Dict
+
+-- * Some type-level naturals
+
+type N0 = Z
+type N1 = S N0
+type N2 = S N1
+type N3 = S N2
+type N4 = S N3
+type N5 = S N4
+type N6 = S N5
+type N7 = S N6
+type N8 = S N7
+type N9 = S N8