diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,31 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
 and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## [1.1.2] - 2026-08-07
+
+### Fixed
+
+- Pass command-line arguments to hspec.
+
+## [1.1.1] - 2026-07-26
+
+### Added
+
+- `modify*` QuickCheck combinators
+- Dependency on `quickcheck-effectful`
+- Ability to run effectful computation in QuickCheck props
+
+## [1.1.0] - 2026-07-21
+
+### Added
+
+- `prop`, `fprop`, `xprop` combinators
+- `runHUnit` re-export
+
+### Removed
+
+- `HasCallStack` and `Spec` re-exports
+
 ## [1.0.1] - 2026-07-13
 
 ### Added
diff --git a/hspec-effectful.cabal b/hspec-effectful.cabal
--- a/hspec-effectful.cabal
+++ b/hspec-effectful.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: hspec-effectful
-version: 1.0.1
+version: 1.1.2
 synopsis: Effectful driver for Hspec
 category: Test
 description:
@@ -26,6 +26,8 @@
     -Wno-missing-import-lists
     -Wno-missing-kind-signatures
     -Wno-all-missed-specialisations
+    -Wno-missing-role-annotations
+    -Wno-term-variable-capture
 
   default-extensions:
     ApplicativeDo
@@ -40,6 +42,7 @@
     FlexibleContexts
     GeneralizedNewtypeDeriving
     ImportQualifiedPost
+    ImpredicativeTypes
     LambdaCase
     NamedFieldPuns
     NoImplicitPrelude
@@ -48,6 +51,7 @@
     OverloadedStrings
     RecordWildCards
     RecursiveDo
+    ScopedTypeVariables
     TypeApplications
     TypeFamilies
     TypeOperators
@@ -56,11 +60,13 @@
   build-depends:
     base >=4.16 && <5,
     effectful >=2.6 && <2.7,
+    quickcheck-effectful >=1.0 && <1.1,
 
 library
   import: common
   hs-source-dirs: src
   build-depends:
+    QuickCheck >=2.15 && <3,
     hspec >=2.11 && <2.12,
     hspec-core >=2.11 && <2.12,
     hspec-expectations >=0.8 && <0.9,
@@ -77,4 +83,5 @@
   hs-source-dirs: test
   main-is: Main.hs
   build-depends:
-    hspec-effectful
+    hspec-effectful,
+    quickcheck-effectful,
diff --git a/src/Effectful/Hspec.hs b/src/Effectful/Hspec.hs
--- a/src/Effectful/Hspec.hs
+++ b/src/Effectful/Hspec.hs
@@ -1,7 +1,4 @@
-{-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE Trustworthy #-}
-{-# OPTIONS_GHC -Wno-missing-role-annotations #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
 
 -- |
 -- Module      : Effectful.Hspec
@@ -36,16 +33,16 @@
 -- >             put $ funds - amount
 -- >             pure True
 --
--- Use 'describe' to group related examples, 'it' to state individual expectations,
--- and setup/teardown combinators such as 'before_', 'after_', or 'around_' to
+-- Use 'describe' to group related examples, 'prop' and 'it' to state individual properties or
+-- expectations ,and setup/teardown combinators such as 'before_', 'after_', or 'around_' to
 -- run the examples from a known initial state:
 --
 -- > accountSpec :: (State Int :> es, Hspec :> es) => Eff es ()
 -- > accountSpec = describe "account" . before_ (put @Int 0) $ do
--- >     it "accumulates deposits" $ do
--- >         deposit 100
--- >         deposit 50
--- >         balance `shouldReturn` 150
+-- >     prop "accumulates deposits" \(Positive a) (Positive b) -> do
+-- >         deposit a
+-- >         deposit b
+-- >         balance `shouldReturn` a + b
 -- >
 -- >     it "checks for sufficient funds before withdrawing" $ do
 -- >         deposit 100
@@ -65,6 +62,7 @@
     , runHspecWith
     , runHspec'
     , runHspec
+    , runHUnit
 
       -- * Spec construction
     , describe
@@ -112,10 +110,20 @@
     , shouldNotReturn
     , shouldThrow
     , anyException
+
+      -- * Properties
+    , modifyArgs
+    , modifyMaxSuccess
+    , modifyMaxDiscardRatio
+    , modifyMaxSize
+    , modifyMaxShrinks
+    , prop
+    , xprop
+    , fprop
+
+      -- * Config
     , Config (..)
     , defaultConfig
-    , Hspec.Spec
-    , HasCallStack
     )
 where
 
@@ -124,15 +132,18 @@
 import Data.Typeable (typeOf)
 import Effectful
 import Effectful.Dispatch.Static
-import Effectful.Environment (runEnvironment, withArgs)
 import Effectful.Exception (Exception, throwIO, try)
-import Effectful.HUnit as HUnit
+import Effectful.HUnit (Assertion, HUnit, runHUnit, (@?=))
+import Effectful.HUnit qualified as HUnit
+import Effectful.QuickCheck (Testable, property, unliftProperty)
 import Test.Hspec qualified as Hspec
 import Test.Hspec.Core.Spec (ResultStatus (..))
 import Test.Hspec.Expectations (Selector, anyException)
 import Test.Hspec.Expectations.Pretty.Matcher (matchList)
+import Test.Hspec.QuickCheck qualified as Hspec
 import Test.Hspec.Runner (Config (..), defaultConfig)
 import Test.Hspec.Runner qualified as Hspec
+import Test.QuickCheck qualified as QuickCheck
 import Prelude
 
 data Hspec :: Effect
@@ -157,7 +168,7 @@
                     }
             . inject
             $ action
-    runEnvironment . withArgs [] . liftIO $ Hspec.hspecWith config spec
+    liftIO $ Hspec.hspecWith config spec
     pure a
 
 runHspecWith :: (IOE :> es) => Config -> Eff (Hspec ': es) a -> Eff es a
@@ -174,160 +185,139 @@
     Hspec{unlift} <- getStaticRep
     unsafeEff_ . unlift . inject $ action
 
+appendSpec :: (Hspec :> es) => Hspec.Spec -> Eff es ()
+appendSpec spec = stateStaticRep \hspec -> ((), hspec{spec = hspec.spec >> spec})
+
 mapSpec :: (HasCallStack, Hspec :> es) => (Hspec.Spec -> Hspec.Spec) -> Eff es a -> Eff es a
 mapSpec f action =
     stateStaticRepM \before -> do
         putStaticRep before{spec = pure ()}
         result <- action
-        after <- getStaticRep
-        pure (result, before{spec = spec before >> f (spec after)})
+        after <- getStaticRep @Hspec
+        pure (result, before{spec = before.spec >> f after.spec})
 
--- | Lifted 'Hspec.describe'
+-- | Lifted 'Hspec.describe'.
 describe :: (HasCallStack, Hspec :> es) => String -> Eff es a -> Eff es a
 describe = mapSpec . Hspec.describe
 
--- | Lifted 'Hspec.it'
+-- | Lifted 'Hspec.it'.
 it :: (HasCallStack, Hspec :> es) => String -> Eff es () -> Eff es ()
 it label action = do
     ioAction <-
         unsafeConcUnliftIO Ephemeral Unlimited \runInIO ->
             pure (runInIO action)
-    stateStaticRep \hspec -> ((), hspec{spec = spec hspec >> Hspec.it label ioAction})
+    appendSpec $ Hspec.it label ioAction
 
--- | Lifted 'Hspec.specify'
+-- | Lifted 'Hspec.specify'.
 specify :: (HasCallStack, Hspec :> es) => String -> Eff es () -> Eff es ()
 specify = it
 
--- | Lifted 'Hspec.context'
+-- | Lifted 'Hspec.context'.
 context :: (HasCallStack, Hspec :> es) => String -> Eff es a -> Eff es a
 context = describe
 
--- | Lifted 'Hspec.pending'
+-- | Lifted 'Hspec.pending'.
 pending :: (HasCallStack, Hspec :> es) => Eff es ()
 pending = getStaticRep @Hspec >> unsafeEff_ Hspec.pending
 
 pending_ :: Eff es ()
 pending_ = throwIO $ Pending Nothing Nothing
 
--- | Lifted 'Hspec.pendingWith'
+-- | Lifted 'Hspec.pendingWith'.
 pendingWith :: (HasCallStack, Hspec :> es) => String -> Eff es ()
 pendingWith = (getStaticRep @Hspec >>) . unsafeEff_ . Hspec.pendingWith
 
--- | Lifted 'Hspec.xit'
+-- | Lifted 'Hspec.xit'.
 xit :: (HasCallStack, Hspec :> es) => String -> Eff es () -> Eff es ()
 xit = (before_ pending_ .) . it
 
--- | Lifted 'Hspec.xspecify'
+-- | Lifted 'Hspec.xspecify'.
 xspecify :: (HasCallStack, Hspec :> es) => String -> Eff es () -> Eff es ()
 xspecify = xit
 
--- | Lifted 'Hspec.xdescribe'
+-- | Lifted 'Hspec.xdescribe'.
 xdescribe :: (HasCallStack, Hspec :> es) => String -> Eff es a -> Eff es a
 xdescribe = (before_ pending_ .) . describe
 
--- | Lifted 'Hspec.xcontext'
+-- | Lifted 'Hspec.xcontext'.
 xcontext :: (HasCallStack, Hspec :> es) => String -> Eff es a -> Eff es a
 xcontext = xdescribe
 
--- | Lifted 'Hspec.focus'
+-- | Lifted 'Hspec.focus'.
 focus :: (HasCallStack, Hspec :> es) => Eff es a -> Eff es a
 focus = mapSpec Hspec.focus
 
--- | Lifted 'Hspec.fit'
+-- | Lifted 'Hspec.fit'.
 fit :: (HasCallStack, Hspec :> es) => String -> Eff es () -> Eff es ()
 fit = fmap focus . it
 
--- | Lifted 'Hspec.fspecify'
+-- | Lifted 'Hspec.fspecify'.
 fspecify :: (HasCallStack, Hspec :> es) => String -> Eff es () -> Eff es ()
 fspecify = fit
 
--- | Lifted 'Hspec.fdescribe'
+-- | Lifted 'Hspec.fdescribe'.
 fdescribe :: (HasCallStack, Hspec :> es) => String -> Eff es a -> Eff es a
 fdescribe = fmap focus . describe
 
--- | Lifted 'Hspec.fcontext'
+-- | Lifted 'Hspec.fcontext'.
 fcontext :: (HasCallStack, Hspec :> es) => String -> Eff es a -> Eff es a
 fcontext = fdescribe
 
--- | Lifted 'Hspec.parallel'
+-- | Lifted 'Hspec.parallel'.
 parallel :: (HasCallStack, Hspec :> es) => Eff es a -> Eff es a
 parallel = mapSpec Hspec.parallel
 
--- | Lifted 'Hspec.sequential'
+-- | Lifted 'Hspec.sequential'.
 sequential :: (HasCallStack, Hspec :> es) => Eff es a -> Eff es a
 sequential = mapSpec Hspec.sequential
 
--- | Lifted 'Hspec.before_'
+-- | Lifted 'Hspec.before_'.
 before_ :: (HasCallStack, Hspec :> es) => Eff es () -> Eff es a -> Eff es a
 before_ setup action = do
     ioSetup <-
         unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
             pure (unlift setup)
-    stateStaticRepM \prev -> do
-        putStaticRep prev{spec = pure ()}
-        result <- action
-        after <- getStaticRep
-        pure (result, prev{spec = spec prev >> Hspec.before_ ioSetup (spec after)})
+    mapSpec (Hspec.before_ ioSetup) action
 
--- | Lifted 'Hspec.beforeAll_'
+-- | Lifted 'Hspec.beforeAll_'.
 beforeAll_ :: (HasCallStack, Hspec :> es) => Eff es () -> Eff es a -> Eff es a
 beforeAll_ setup action = do
     ioSetup <-
         unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
             pure (unlift setup)
-    stateStaticRepM \prev -> do
-        putStaticRep prev{spec = pure ()}
-        result <- action
-        after <- getStaticRep
-        pure (result, prev{spec = spec prev >> Hspec.beforeAll_ ioSetup (spec after)})
+    mapSpec (Hspec.beforeAll_ ioSetup) action
 
--- | Lifted 'Hspec.after_'
+-- | Lifted 'Hspec.after_'.
 after_ :: (HasCallStack, Hspec :> es) => Eff es () -> Eff es a -> Eff es a
 after_ teardown action = do
     ioTeardown <-
         unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
             pure (unlift teardown)
-    stateStaticRepM \prev -> do
-        putStaticRep prev{spec = pure ()}
-        result <- action
-        after <- getStaticRep
-        pure (result, prev{spec = spec prev >> Hspec.after_ ioTeardown (spec after)})
+    mapSpec (Hspec.after_ ioTeardown) action
 
--- | Lifted 'Hspec.afterAll_'
+-- | Lifted 'Hspec.afterAll_'.
 afterAll_ :: (HasCallStack, Hspec :> es) => Eff es () -> Eff es a -> Eff es a
 afterAll_ teardown action = do
     ioTeardown <-
         unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
             pure (unlift teardown)
-    stateStaticRepM \prev -> do
-        putStaticRep prev{spec = pure ()}
-        result <- action
-        after <- getStaticRep
-        pure (result, prev{spec = spec prev >> Hspec.afterAll_ ioTeardown (spec after)})
+    mapSpec (Hspec.afterAll_ ioTeardown) action
 
--- | Lifted 'Hspec.around_'
+-- | Lifted 'Hspec.around_'.
 around_ :: (HasCallStack, Hspec :> es) => (Eff es () -> Eff es ()) -> Eff es a -> Eff es a
 around_ wrapper action = do
     ioWrapper <-
         unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
             pure (unlift . wrapper . unsafeEff_)
-    stateStaticRepM \prev -> do
-        putStaticRep prev{spec = pure ()}
-        result <- action
-        after <- getStaticRep
-        pure (result, prev{spec = spec prev >> Hspec.around_ ioWrapper (spec after)})
+    mapSpec (Hspec.around_ ioWrapper) action
 
--- | Lifted 'Hspec.aroundAll_'
+-- | Lifted 'Hspec.aroundAll_'.
 aroundAll_ :: (HasCallStack, Hspec :> es) => (Eff es () -> Eff es ()) -> Eff es a -> Eff es a
 aroundAll_ wrapper action = do
     ioWrapper <-
         unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
             pure (unlift . wrapper . unsafeEff_)
-    stateStaticRepM \prev -> do
-        putStaticRep prev{spec = pure ()}
-        result <- action
-        after <- getStaticRep
-        pure (result, prev{spec = spec prev >> Hspec.aroundAll_ ioWrapper (spec after)})
+    mapSpec (Hspec.aroundAll_ ioWrapper) action
 
 expectationFailure :: (HasCallStack, Hspec :> es) => String -> Expectation es
 expectationFailure msg = hunit $ HUnit.assertFailure msg
@@ -350,14 +340,12 @@
 
 infix 1 `shouldNotBe`, `shouldNotSatisfy`, `shouldNotContain`, `shouldNotReturn`
 
--- |
--- @actual \`shouldBe\` expected@ sets the expectation that @actual@ is equal
+-- | @actual \`shouldBe\` expected@ sets the expectation that @actual@ is equal
 -- to @expected@.
 shouldBe :: (HasCallStack, Show a, Eq a, Hspec :> es) => a -> a -> Expectation es
 actual `shouldBe` expected = hunit $ actual @?= expected
 
--- |
--- @v \`shouldSatisfy\` p@ sets the expectation that @p v@ is @True@.
+-- | @v \`shouldSatisfy\` p@ sets the expectation that @p v@ is @True@.
 shouldSatisfy :: (HasCallStack, Show a, Hspec :> es) => a -> (a -> Bool) -> Expectation es
 v `shouldSatisfy` p = expectTrue ("predicate failed on: " ++ show v) (p v)
 
@@ -372,55 +360,46 @@
   where
     errorMsg = show result ++ " " ++ errorDesc ++ " " ++ show expected
 
--- |
--- @list \`shouldStartWith\` prefix@ sets the expectation that @list@ starts with @prefix@,
+-- | @list \`shouldStartWith\` prefix@ sets the expectation that @list@ starts with @prefix@.
 shouldStartWith :: (HasCallStack, Show a, Eq a, Hspec :> es) => [a] -> [a] -> Expectation es
 shouldStartWith = compareWith List.isPrefixOf "does not start with"
 
--- |
--- @list \`shouldEndWith\` suffix@ sets the expectation that @list@ ends with @suffix@,
+-- | @list \`shouldEndWith\` suffix@ sets the expectation that @list@ ends with @suffix@.
 shouldEndWith :: (HasCallStack, Show a, Eq a, Hspec :> es) => [a] -> [a] -> Expectation es
 shouldEndWith = compareWith List.isSuffixOf "does not end with"
 
--- |
--- @list \`shouldContain\` sublist@ sets the expectation that @sublist@ is contained,
+-- | @list \`shouldContain\` sublist@ sets the expectation that @sublist@ is contained,
 -- wholly and intact, anywhere in @list@.
 shouldContain :: (HasCallStack, Show a, Eq a, Hspec :> es) => [a] -> [a] -> Expectation es
 shouldContain = compareWith List.isInfixOf "does not contain"
 
--- |
--- @xs \`shouldMatchList\` ys@ sets the expectation that @xs@ has the same
--- elements that @ys@ has, possibly in another order
+-- | @xs \`shouldMatchList\` ys@ sets the expectation that @xs@ has the same
+-- elements that @ys@ has, possibly in another order.
 shouldMatchList :: (HasCallStack, Show a, Eq a, Hspec :> es) => [a] -> [a] -> Expectation es
 xs `shouldMatchList` ys = maybe (return ()) expectationFailure (matchList xs ys)
 
--- |
--- @action \`shouldReturn\` expected@ sets the expectation that @action@
+-- | @action \`shouldReturn\` expected@ sets the expectation that @action@
 -- returns @expected@.
 shouldReturn :: (HasCallStack, Show a, Eq a, Hspec :> es) => Eff es a -> a -> Expectation es
 action `shouldReturn` expected = action >>= (`shouldBe` expected)
 
--- |
--- @actual \`shouldNotBe\` notExpected@ sets the expectation that @actual@ is not
--- equal to @notExpected@
+-- | @actual \`shouldNotBe\` notExpected@ sets the expectation that @actual@ is not
+-- equal to @notExpected@.
 shouldNotBe :: (HasCallStack, Show a, Eq a, Hspec :> es) => a -> a -> Expectation es
 actual `shouldNotBe` notExpected = expectTrue ("not expected: " ++ show actual) (actual /= notExpected)
 
--- |
--- @v \`shouldNotSatisfy\` p@ sets the expectation that @p v@ is @False@.
+-- | @v \`shouldNotSatisfy\` p@ sets the expectation that @p v@ is @False@.
 shouldNotSatisfy :: (HasCallStack, Show a, Hspec :> es) => a -> (a -> Bool) -> Expectation es
 v `shouldNotSatisfy` p = expectTrue ("predicate succeeded on: " ++ show v) ((not . p) v)
 
--- |
--- @list \`shouldNotContain\` sublist@ sets the expectation that @sublist@ is not
+-- | @list \`shouldNotContain\` sublist@ sets the expectation that @sublist@ is not
 -- contained anywhere in @list@.
 shouldNotContain :: (HasCallStack, Show a, Eq a, Hspec :> es) => [a] -> [a] -> Expectation es
 list `shouldNotContain` sublist = expectTrue errorMsg (not $ sublist `List.isInfixOf` list)
   where
     errorMsg = show list ++ " does contain " ++ show sublist
 
--- |
--- @action \`shouldNotReturn\` notExpected@ sets the expectation that @action@
+-- | @action \`shouldNotReturn\` notExpected@ sets the expectation that @action@
 -- does not return @notExpected@.
 shouldNotReturn
     :: (HasCallStack, Show a, Eq a, Hspec :> es)
@@ -429,8 +408,7 @@
     -> Expectation es
 action `shouldNotReturn` notExpected = action >>= (`shouldNotBe` notExpected)
 
--- |
--- @action \`shouldThrow\` selector@ sets the expectation that @action@ throws
+-- | @action \`shouldThrow\` selector@ sets the expectation that @action@ throws
 -- an exception.  The precise nature of the expected exception is described
 -- with a 'Selector'.
 shouldThrow
@@ -453,3 +431,48 @@
       where
         instanceOf :: Selector a -> a
         instanceOf _ = error "Effectful.Hspec.shouldThrow: broken Typeable instance"
+
+-- | Lifted 'Hspec.modifyArgs'.
+modifyArgs
+    :: (HasCallStack, Hspec :> es)
+    => (QuickCheck.Args -> QuickCheck.Args)
+    -> Eff es a
+    -> Eff es a
+modifyArgs = mapSpec . Hspec.modifyArgs
+
+-- | Lifted 'Hspec.modifyMaxSuccess'.
+modifyMaxSuccess :: (HasCallStack, Hspec :> es) => (Int -> Int) -> Eff es a -> Eff es a
+modifyMaxSuccess = mapSpec . Hspec.modifyMaxSuccess
+
+-- | Lifted 'Hspec.modifyMaxDiscardRatio'.
+modifyMaxDiscardRatio :: (HasCallStack, Hspec :> es) => (Int -> Int) -> Eff es a -> Eff es a
+modifyMaxDiscardRatio = mapSpec . Hspec.modifyMaxDiscardRatio
+
+-- | Lifted 'Hspec.modifyMaxSize'.
+modifyMaxSize :: (HasCallStack, Hspec :> es) => (Int -> Int) -> Eff es a -> Eff es a
+modifyMaxSize = mapSpec . Hspec.modifyMaxSize
+
+-- | Lifted 'Hspec.modifyMaxSize'.
+modifyMaxShrinks :: (HasCallStack, Hspec :> es) => (Int -> Int) -> Eff es a -> Eff es a
+modifyMaxShrinks = mapSpec . Hspec.modifyMaxShrinks
+
+appendProp
+    :: (HasCallStack, Testable prop es, Hspec :> es)
+    => (QuickCheck.Property -> Hspec.Spec)
+    -> prop
+    -> Eff es ()
+appendProp f p =
+    appendSpec . f =<< unsafeConcUnliftIO Ephemeral Unlimited \unlift ->
+        pure . unliftProperty unlift . property $ p
+
+-- | Lifted 'Hspec.prop'.
+prop :: (HasCallStack, Testable prop es, Hspec :> es) => String -> prop -> Eff es ()
+prop = appendProp . Hspec.prop
+
+-- | Lifted 'Hspec.xprop'.
+xprop :: (HasCallStack, Testable prop es, Hspec :> es) => String -> prop -> Eff es ()
+xprop = appendProp . Hspec.xprop
+
+-- | Lifted 'Hspec.fprop'.
+fprop :: (HasCallStack, Testable prop es, Hspec :> es) => String -> prop -> Eff es ()
+fprop = appendProp . Hspec.fprop
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,11 +1,16 @@
 {-# OPTIONS_GHC -Wno-missing-local-signatures #-}
 {-# OPTIONS_GHC -Wno-monomorphism-restriction #-}
+{-# OPTIONS_GHC -Wno-name-shadowing #-}
 {-# OPTIONS_GHC -Wno-type-defaults #-}
 
+{- HLINT ignore "Redundant reverse" -}
+
 module Main where
 
 import Effectful
 import Effectful.Hspec
+import Effectful.QuickCheck ((.&&.), (===))
+import Effectful.State.Static.Local (evalState, get, modify)
 import Prelude
 
 main :: IO ()
@@ -49,3 +54,12 @@
     it "handles shouldNotReturn" $ do
         let action = pure (1 :: Int) :: Eff es Int
         action `shouldNotReturn` 2
+
+    prop "pure prop" \(xs :: [Int]) ->
+        (reverse . reverse) xs == xs
+
+    prop "eff prop" \(n :: Int) ->
+        evalState n do
+            modify @Int (+ 1)
+            x <- get
+            pure $ (x === n + 1) .&&. (x > n)