From ffa91484573a2c2be3f6ae2190c768e7a77e8b5c Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 3 Apr 2024 15:06:52 +0200 Subject: Simple usage example --- src/Data/Array/Nested/Internal.hs | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Data/Array/Nested') 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 -- cgit v1.2.3-70-g09d2