Fix f in SMayNat to always be SNat and UNPACK it

1 files changed, 5 insertions, 5 deletions

diff --git a/README.md b/README.md
index 8393148..667bf9d 100644
--- a/README.md
+++ b/README.md
@@ -112,18 +112,18 @@ data ShS sh where
 
 data IShX xsh where
   ZSX   :: IShX '[]
-  (:$%) :: SMayNat Int SNat mn -> IShX xsh -> IShX (mn : xsh)
+  (:$%) :: SMayNat Int mn -> IShX xsh -> IShX (mn : xsh)
 -- where:
-data SMayNat i f n where
-  SUnknown :: i   -> SMayNat i f Nothing
-  SKnown   :: f n -> SMayNat i f (Just n)
+data SMayNat i n where
+  SUnknown :: i   -> SMayNat i Nothing
+  SKnown   :: SNat n -> SMayNat i (Just n)
 
 -- Occasionally one needs a singleton for only the _known_ dimensions of a mixed
 -- shape -- that is to say, only the statically-known part of a mixed shape.
 -- StaticShX provides for this need. It can be used as if defined as follows:
 data StaticShX xsh where
   ZKX   :: StaticShX '[]
-  (:!%) :: SMayNat () SNat mn -> StaticShX xsh -> StaticShX (mn : xsh)
+  (:!%) :: SMayNat () mn -> StaticShX xsh -> StaticShX (mn : xsh)
 
 -- The Elt class describes types that can be used as elements of an array. While
 -- it is technically possible to define new instances of this class, typical