diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,11 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v1.3.1 _(2024-07-12)_
+
+### Added
+- Added `count` in `Language.Hasmtlib.Counting`
+
 ## v1.3.0 _(2024-07-12)_
 
 ### Added
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.3.0
+version:               1.3.1
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs
--- a/src/Language/Hasmtlib/Counting.hs
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -6,18 +6,27 @@
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Iteable
+import Data.Proxy
 
+count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t
+count' _ = sum . fmap (\b -> ite b 1 0)
+{-# INLINEABLE count' #-}
+
+count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
+count = count' (Proxy @t)
+{-# INLINE count #-}
+
 -- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'
 atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
-atMost  k = (<=? k) . sum . fmap (\b -> ite b 1 0)
+atMost  k = (<=? k) . count
 {-# INLINEABLE atMost #-}
 
 -- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'
 atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
-atLeast k = (>=? k) . sum . fmap (\b -> ite b 1 0)
+atLeast k = (>=? k) . count
 {-# INLINEABLE atLeast #-}
 
 -- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'
 exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
-exactly k = (=== k) . sum . fmap (\b -> ite b 1 0)
+exactly k = (=== k) . count
 {-# INLINEABLE exactly #-}