diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Revision history for natural-arithmetic
 
+## 0.2.1.0 -- 2024-02-02
+
+* Add `fromInt` and `fromInt#` to `Arithmetic.Fin`.
+* Update package metadata.
+
 ## 0.2.0.0 -- 2024-01-09
 
 * Change the types of `with#` and `construct#` (both in `Arithmetic.Fin`)
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal
--- a/natural-arithmetic.cabal
+++ b/natural-arithmetic.cabal
@@ -1,7 +1,7 @@
-cabal-version: 2.2
-name: natural-arithmetic
-version: 0.2.0.0
-synopsis: Arithmetic of natural numbers
+cabal-version:   2.2
+name:            natural-arithmetic
+version:         0.2.1.0
+synopsis:        Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals
   no shortage of libraries for handling the arithmetic of natural
@@ -18,7 +18,7 @@
   application code, not in library code. This is because libraries
   should not require the presence of typechecker plugins. Technically,
   they can (you could document it), but many developers will not
-  use libraries that have unusual install procedures like this. 
+  use libraries that have unusual install procedures like this.
   .
   This library, in places, requires users to use the 'TypeApplications`
   language extension. This is done when a number is only need at
@@ -28,7 +28,7 @@
   in `Arithmetic.Lt` and `Arithmetic.Lte`. This is done in the interest
   of making it easy for user to assemble proofs. Recall that proof
   assembly is done by hand rather than by an SMT solver, so removing
-  some tediousness from this is helpful to users. 
+  some tediousness from this is helpful to users.
   .
   This library provides left and variants variants of several functions.
   For example, `Arithmetic.Lte` provides both `substituteL` and
@@ -54,29 +54,40 @@
   * Decrement: Decrease an upper bound along with the bounded value
   .
   * Substitute: Replace a number with an equal number
-homepage: https://github.com/andrewthad/natural-arithmetic
-bug-reports: https://github.com/andrewthad/natural-arithmetic/issues
-license: BSD-3-Clause
-license-file: LICENSE
-author: Andrew Martin
-maintainer: andrew.thaddeus@gmail.com
-copyright: 2019 Andrew Martin
-category: Math
-extra-source-files: CHANGELOG.md
 
+homepage:        https://github.com/byteverse/natural-arithmetic
+bug-reports:     https://github.com/byteverse/natural-arithmetic/issues
+license:         BSD-3-Clause
+license-file:    LICENSE
+author:          Andrew Martin
+maintainer:      amartin@layer3com.com
+copyright:       2019 Andrew Martin
+category:        Math
+extra-doc-files: CHANGELOG.md
+
+common build-settings
+  default-language: Haskell2010
+  ghc-options:      -Wall -Wunused-packages
+
 library
+  import:          build-settings
   exposed-modules:
-    Arithmetic.Fin
     Arithmetic.Equal
+    Arithmetic.Fin
     Arithmetic.Lt
     Arithmetic.Lte
     Arithmetic.Nat
+    Arithmetic.Plus
     Arithmetic.Types
     Arithmetic.Unsafe
-    Arithmetic.Plus
+
   build-depends:
-    , base>=4.14 && <5
-    , unlifted >=0.2.1
-  hs-source-dirs: src
-  default-language: Haskell2010
-  ghc-options: -Wall -O2
+    , base      >=4.14  && <5
+    , unlifted  >=0.2.1
+
+  hs-source-dirs:  src
+  ghc-options:     -O2
+
+source-repository head
+  type:     git
+  location: git://github.com/byteverse/natural-arithmetic.git
diff --git a/src/Arithmetic/Equal.hs b/src/Arithmetic/Equal.hs
--- a/src/Arithmetic/Equal.hs
+++ b/src/Arithmetic/Equal.hs
@@ -1,9 +1,9 @@
-{-# language DataKinds #-}
-{-# language ExplicitForAll #-}
-{-# language KindSignatures #-}
-{-# language MagicHash #-}
-{-# language TypeOperators #-}
-{-# language UnboxedTuples #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
 
 module Arithmetic.Equal
   ( symmetric
@@ -14,29 +14,29 @@
   , lift
   ) where
 
-import Arithmetic.Unsafe (type (:=:)(Eq), type (:=:#)(Eq#))
+import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#))
 import GHC.TypeNats (type (+))
 
 symmetric :: (m :=: n) -> (n :=: m)
-{-# inline symmetric #-}
+{-# INLINE symmetric #-}
 symmetric Eq = Eq
 
 plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)
-{-# inline plusL #-}
+{-# INLINE plusL #-}
 plusL Eq = Eq
 
 plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)
-{-# inline plusR #-}
+{-# INLINE plusR #-}
 plusR Eq = Eq
 
 plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n)
-{-# inline plusL# #-}
+{-# INLINE plusL# #-}
 plusL# _ = Eq# (# #)
 
 plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c)
-{-# inline plusR# #-}
+{-# INLINE plusR# #-}
 plusR# _ = Eq# (# #)
 
 lift :: (m :=:# n) -> (m :=: n)
-{-# inline lift #-}
+{-# INLINE lift #-}
 lift _ = Eq
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -1,15 +1,15 @@
-{-# language BangPatterns #-}
-{-# language DataKinds #-}
-{-# language ExplicitNamespaces #-}
-{-# language GADTs #-}
-{-# language KindSignatures #-}
-{-# language MagicHash #-}
-{-# language PatternSynonyms #-}
-{-# language RankNTypes #-}
-{-# language ScopedTypeVariables #-}
-{-# language TypeApplications #-}
-{-# language TypeOperators #-}
-{-# language UnboxedTuples #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
+
 module Arithmetic.Fin
   ( -- * Modification
     incrementL
@@ -20,7 +20,9 @@
   , weakenR
   , succ
   , succ#
+
     -- * Traverse
+
     -- | These use the terms @ascend@ and @descend@ rather than the
     -- more popular @l@ (left) and @r@ (right) that pervade the Haskell
     -- ecosystem. The general rule is that ascending functions pair
@@ -43,178 +45,218 @@
   , descending
   , ascendingSlice
   , descendingSlice
+
     -- * Absurdities
   , absurd
+
     -- * Demote
   , demote
   , demote#
+
     -- * Deconstruct
   , with
   , with#
+
     -- * Construct
   , construct#
   , remInt#
   , remWord#
+  , fromInt
+  , fromInt#
+
     -- * Lift and Unlift
   , lift
   , unlift
   ) where
 
-import Prelude hiding (last,succ)
+import Prelude hiding (last, succ)
 
 import Arithmetic.Nat ((<?))
-import Arithmetic.Types (Fin(..),Difference(..),Nat,Nat#,type (<), type (<#), type (<=), type (:=:))
-import Arithmetic.Types (pattern MaybeFinNothing#, pattern MaybeFinJust#)
-import Arithmetic.Unsafe (Nat#(Nat#),Fin#(Fin#),MaybeFin#)
-import GHC.Exts (Int(I#),(+#),Int#,Word#)
+import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=))
+import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#))
+import GHC.Exts (Int (I#), Int#, Word#, (+#))
 import GHC.TypeNats (type (+))
 
+import qualified Arithmetic.Equal as Eq
 import qualified Arithmetic.Lt as Lt
 import qualified Arithmetic.Lte as Lte
-import qualified Arithmetic.Equal as Eq
 import qualified Arithmetic.Nat as Nat
 import qualified Arithmetic.Plus as Plus
 import qualified Arithmetic.Unsafe as Unsafe
 import qualified GHC.Exts as Exts
 
--- | Raise the index by @m@ and weaken the bound by @m@, adding
--- @m@ to the right-hand side of @n@.
+{- | Raise the index by @m@ and weaken the bound by @m@, adding
+@m@ to the right-hand side of @n@.
+-}
 incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)
-{-# inline incrementR #-}
+{-# INLINE incrementR #-}
 incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf)
 
 incrementR# :: forall n m. Nat# m -> Fin# n -> Fin# (n + m)
-{-# inline incrementR# #-}
+{-# INLINE incrementR# #-}
 incrementR# (Nat# n) (Fin# i) = Fin# (n +# i)
 
--- | Raise the index by @m@ and weaken the bound by @m@, adding
--- @m@ to the left-hand side of @n@.
+{- | Raise the index by @m@ and weaken the bound by @m@, adding
+@m@ to the left-hand side of @n@.
+-}
 incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)
-{-# inline incrementL #-}
+{-# INLINE incrementL #-}
 incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf)
 
--- | Weaken the bound by @m@, adding it to the left-hand side of
--- the existing bound. This does not change the index.
+{- | Weaken the bound by @m@, adding it to the left-hand side of
+the existing bound. This does not change the index.
+-}
 weakenL :: forall n m. Fin n -> Fin (m + n)
-{-# inline weakenL #-}
-weakenL (Fin i pf) = Fin i
-  ( Lt.substituteR
-    (Plus.commutative @n @m)
-    (Lt.plus pf (Lte.zero @m))
-  )
+{-# INLINE weakenL #-}
+weakenL (Fin i pf) =
+  Fin
+    i
+    ( Lt.substituteR
+        (Plus.commutative @n @m)
+        (Lt.plus pf (Lte.zero @m))
+    )
 
--- | Weaken the bound by @m@, adding it to the right-hand side of
--- the existing bound. This does not change the index.
+{- | Weaken the bound by @m@, adding it to the right-hand side of
+the existing bound. This does not change the index.
+-}
 weakenR :: forall n m. Fin n -> Fin (n + m)
-{-# inline weakenR #-}
+{-# INLINE weakenR #-}
 weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero)
 
--- | Weaken the bound, replacing it by another number greater than
--- or equal to itself. This does not change the index.
+{- | Weaken the bound, replacing it by another number greater than
+or equal to itself. This does not change the index.
+-}
 weaken :: forall n m. (n <= m) -> Fin n -> Fin m
-{-# inline weaken #-}
+{-# INLINE weaken #-}
 weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt)
 
 -- | A finite set of no values is impossible.
 absurd :: Fin 0 -> void
-{-# inline absurd #-}
+{-# INLINE absurd #-}
 absurd (Fin _ pf) = Lt.absurd pf
 
--- | Fold over the numbers bounded by @n@ in descending
--- order. This is lazy in the accumulator. For convenince,
--- this differs from @foldr@ in the order of the parameters.
---
--- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
-descend :: forall a n.
-     Nat n -- ^ Upper bound
-  -> a -- ^ Initial accumulator
-  -> (Fin n -> a -> a) -- ^ Update accumulator
-  -> a
-{-# inline descend #-}
+{- | Fold over the numbers bounded by @n@ in descending
+order. This is lazy in the accumulator. For convenince,
+this differs from @foldr@ in the order of the parameters.
+
+> descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
+-}
+descend ::
+  forall a n.
+  -- | Upper bound
+  Nat n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin n -> a -> a) ->
+  a
+{-# INLINE descend #-}
 descend !n b0 f = go Nat.zero
-  where
+ where
   go :: Nat m -> a
   go !m = case m <? n of
     Nothing -> b0
     Just lt -> f (Fin m lt) (go (Nat.succ m))
 
-descend# :: forall a n.
-     Nat# n -- ^ Upper bound
-  -> a -- ^ Initial accumulator
-  -> (Fin# n -> a -> a) -- ^ Update accumulator
-  -> a
-{-# inline descend# #-}
+descend# ::
+  forall a n.
+  -- | Upper bound
+  Nat# n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin# n -> a -> a) ->
+  a
+{-# INLINE descend# #-}
 descend# !n b0 f = descend (Nat.lift n) b0 (\ix a -> f (unlift ix) a)
 
--- | Fold over the numbers bounded by @n@ in descending
--- order. This is strict in the accumulator. For convenince,
--- this differs from @foldr'@ in the order of the parameters.
---
--- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
-descend' :: forall a n.
-     Nat n -- ^ Upper bound
-  -> a -- ^ Initial accumulator
-  -> (Fin n -> a -> a) -- ^ Update accumulator
-  -> a
-{-# inline descend' #-}
+{- | Fold over the numbers bounded by @n@ in descending
+order. This is strict in the accumulator. For convenince,
+this differs from @foldr'@ in the order of the parameters.
+
+> descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))
+-}
+descend' ::
+  forall a n.
+  -- | Upper bound
+  Nat n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin n -> a -> a) ->
+  a
+{-# INLINE descend' #-}
 descend' !n !b0 f = go n Lte.reflexive b0
-  where
-    go :: Nat p -> p <= n -> a -> a
-    go !m pLteEn !b = case Nat.monus m Nat.one of
-      Nothing -> b
-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
-        let !cLtEn = descendLemma cPlusOneEqP pLteEn
-        in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b)
+ where
+  go :: Nat p -> p <= n -> a -> a
+  go !m pLteEn !b = case Nat.monus m Nat.one of
+    Nothing -> b
+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+      let !cLtEn = descendLemma cPlusOneEqP pLteEn
+       in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b)
 
--- | Fold over the numbers bounded by @n@ in ascending order. This
--- is lazy in the accumulator.
---
--- > ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))
-ascend :: forall a n.
-     Nat n
-  -> a
-  -> (Fin n -> a -> a)
-  -> a
-{-# inline ascend #-}
+{- | Fold over the numbers bounded by @n@ in ascending order. This
+is lazy in the accumulator.
+
+> ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))
+-}
+ascend ::
+  forall a n.
+  Nat n ->
+  a ->
+  (Fin n -> a -> a) ->
+  a
+{-# INLINE ascend #-}
 ascend !n !b0 f = go n Lte.reflexive
-  where
-    go :: Nat p -> (p <= n) -> a
-    go !m pLteEn = case Nat.monus m Nat.one of
-      Nothing -> b0
-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
-        let !cLtEn = descendLemma cPlusOneEqP pLteEn
-        in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn))
+ where
+  go :: Nat p -> (p <= n) -> a
+  go !m pLteEn = case Nat.monus m Nat.one of
+    Nothing -> b0
+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+      let !cLtEn = descendLemma cPlusOneEqP pLteEn
+       in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn))
 
--- | Strict fold over the numbers bounded by @n@ in ascending
--- order. For convenince, this differs from @foldl'@ in the
--- order of the parameters.
---
--- > ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))
-ascend' :: forall a n.
-     Nat n -- ^ Upper bound
-  -> a -- ^ Initial accumulator
-  -> (Fin n -> a -> a) -- ^ Update accumulator
-  -> a
-{-# inline ascend' #-}
+{- | Strict fold over the numbers bounded by @n@ in ascending
+order. For convenince, this differs from @foldl'@ in the
+order of the parameters.
+
+> ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))
+-}
+ascend' ::
+  forall a n.
+  -- | Upper bound
+  Nat n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin n -> a -> a) ->
+  a
+{-# INLINE ascend' #-}
 ascend' !n !b0 f = go Nat.zero b0
-  where
+ where
   go :: Nat m -> a -> a
   go !m !b = case m <? n of
     Nothing -> b
     Just lt -> go (Nat.succ m) (f (Fin m lt) b)
 
--- | Generalization of @ascend'@ that lets the caller pick the starting index:
---
--- > ascend' === ascendFrom' 0
-ascendFrom' :: forall a m n.
-     Nat m -- ^ Index to start at
-  -> Nat n -- ^ Number of steps to take
-  -> a -- ^ Initial accumulator
-  -> (Fin (m + n) -> a -> a) -- ^ Update accumulator
-  -> a
-{-# inline ascendFrom' #-}
+{- | Generalization of @ascend'@ that lets the caller pick the starting index:
+
+> ascend' === ascendFrom' 0
+-}
+ascendFrom' ::
+  forall a m n.
+  -- | Index to start at
+  Nat m ->
+  -- | Number of steps to take
+  Nat n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin (m + n) -> a -> a) ->
+  a
+{-# INLINE ascendFrom' #-}
 ascendFrom' !m0 !n !b0 f = go m0 b0
-  where
+ where
   end = Nat.plus m0 n
   go :: Nat k -> a -> a
   go !m !b = case m <? end of
@@ -222,259 +264,337 @@
     Just lt -> go (Nat.succ m) (f (Fin m lt) b)
 
 -- | Variant of @ascendFrom'@ with unboxed arguments.
-ascendFrom'# :: forall a m n.
-     Nat# m -- ^ Index to start at
-  -> Nat# n -- ^ Number of steps to take
-  -> a -- ^ Initial accumulator
-  -> (Fin# (m + n) -> a -> a) -- ^ Update accumulator
-  -> a
-{-# inline ascendFrom'# #-}
+ascendFrom'# ::
+  forall a m n.
+  -- | Index to start at
+  Nat# m ->
+  -- | Number of steps to take
+  Nat# n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin# (m + n) -> a -> a) ->
+  a
+{-# INLINE ascendFrom'# #-}
 ascendFrom'# !m0 !n !b0 f = ascendFrom' (Nat.lift m0) (Nat.lift n) b0 (\ix -> f (unlift ix))
 
--- | Strict monadic left fold over the numbers bounded by @n@
--- in ascending order. Roughly:
---
--- > ascendM 4 z0 f =
--- >   f 0 z0 >>= \z1 ->
--- >   f 1 z1 >>= \z2 ->
--- >   f 2 z2 >>= \z3 ->
--- >   f 3 z3
-ascendM :: forall m a n. Monad m
-  => Nat n -- ^ Upper bound
-  -> a -- ^ Initial accumulator
-  -> (Fin n -> a -> m a) -- ^ Update accumulator
-  -> m a
-{-# inline ascendM #-}
+{- | Strict monadic left fold over the numbers bounded by @n@
+in ascending order. Roughly:
+
+> ascendM 4 z0 f =
+>   f 0 z0 >>= \z1 ->
+>   f 1 z1 >>= \z2 ->
+>   f 2 z2 >>= \z3 ->
+>   f 3 z3
+-}
+ascendM ::
+  forall m a n.
+  (Monad m) =>
+  -- | Upper bound
+  Nat n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin n -> a -> m a) ->
+  m a
+{-# INLINE ascendM #-}
 ascendM !n !b0 f = go Nat.zero b0
-  where
+ where
   go :: Nat p -> a -> m a
   go !m !b = case m <? n of
     Nothing -> pure b
     Just lt -> go (Nat.succ m) =<< f (Fin m lt) b
 
--- | Variant of @ascendM@ that takes an unboxed Nat and provides
--- an unboxed Fin to the callback.
-ascendM# :: forall m a n. Monad m
-  => Nat# n -- ^ Upper bound
-  -> a -- ^ Initial accumulator
-  -> (Fin# n -> a -> m a) -- ^ Update accumulator
-  -> m a
-{-# inline ascendM# #-}
+{- | Variant of @ascendM@ that takes an unboxed Nat and provides
+an unboxed Fin to the callback.
+-}
+ascendM# ::
+  forall m a n.
+  (Monad m) =>
+  -- | Upper bound
+  Nat# n ->
+  -- | Initial accumulator
+  a ->
+  -- | Update accumulator
+  (Fin# n -> a -> m a) ->
+  m a
+{-# INLINE ascendM# #-}
 ascendM# n !a0 f = ascendM (Nat.lift n) a0 (\ix a -> f (unlift ix) a)
 
--- | Monadic traversal of the numbers bounded by @n@
--- in ascending order.
---
--- > ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3
-ascendM_ :: forall m a n. Applicative m
-  => Nat n -- ^ Upper bound
-  -> (Fin n -> m a) -- ^ Effectful interpretion
-  -> m ()
-{-# inline ascendM_ #-}
+{- | Monadic traversal of the numbers bounded by @n@
+in ascending order.
+
+> ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3
+-}
+ascendM_ ::
+  forall m a n.
+  (Applicative m) =>
+  -- | Upper bound
+  Nat n ->
+  -- | Effectful interpretion
+  (Fin n -> m a) ->
+  m ()
+{-# INLINE ascendM_ #-}
 ascendM_ !n f = go Nat.zero
-  where
+ where
   go :: Nat p -> m ()
   go !m = case m <? n of
     Nothing -> pure ()
     Just lt -> f (Fin m lt) *> go (Nat.succ m)
 
--- | Variant of @ascendM_@ that takes an unboxed Nat and provides
--- an unboxed Fin to the callback.
-ascendM_# :: forall m a n. Monad m
-  => Nat# n -- ^ Upper bound
-  -> (Fin# n -> m a) -- ^ Update accumulator
-  -> m ()
-{-# inline ascendM_# #-}
+{- | Variant of @ascendM_@ that takes an unboxed Nat and provides
+an unboxed Fin to the callback.
+-}
+ascendM_# ::
+  forall m a n.
+  (Monad m) =>
+  -- | Upper bound
+  Nat# n ->
+  -- | Update accumulator
+  (Fin# n -> m a) ->
+  m ()
+{-# INLINE ascendM_# #-}
 ascendM_# n f = ascendM_ (Nat.lift n) (\ix -> f (unlift ix))
 
 descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c
-{-# inline descendLemma #-}
-descendLemma !aPlusOneEqB !bLteC = id
-  $ Lt.transitiveNonstrictR
-      (Lt.substituteR (Plus.commutative @1 @a)
-      (Lt.plus Lt.zero Lte.reflexive))
-  $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC
+{-# INLINE descendLemma #-}
+descendLemma !aPlusOneEqB !bLteC =
+  id
+    $ Lt.transitiveNonstrictR
+      ( Lt.substituteR
+          (Plus.commutative @1 @a)
+          (Lt.plus Lt.zero Lte.reflexive)
+      )
+    $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC
 
--- | Strict monadic left fold over the numbers bounded by @n@
--- in descending order. Roughly:
---
--- > descendM 4 z f =
--- >   f 3 z0 >>= \z1 ->
--- >   f 2 z1 >>= \z2 ->
--- >   f 1 z2 >>= \z3 ->
--- >   f 0 z3
-descendM :: forall m a n. Monad m
-  => Nat n
-  -> a
-  -> (Fin n -> a -> m a)
-  -> m a
-{-# inline descendM #-}
+{- | Strict monadic left fold over the numbers bounded by @n@
+in descending order. Roughly:
+
+> descendM 4 z f =
+>   f 3 z0 >>= \z1 ->
+>   f 2 z1 >>= \z2 ->
+>   f 1 z2 >>= \z3 ->
+>   f 0 z3
+-}
+descendM ::
+  forall m a n.
+  (Monad m) =>
+  Nat n ->
+  a ->
+  (Fin n -> a -> m a) ->
+  m a
+{-# INLINE descendM #-}
 descendM !n !b0 f = go n Lte.reflexive b0
-  where
-    go :: Nat p -> p <= n -> a -> m a
-    go !m pLteEn !b = case Nat.monus m Nat.one of
-      Nothing -> pure b
-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
-        let !cLtEn = descendLemma cPlusOneEqP pLteEn
-        in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b
+ where
+  go :: Nat p -> p <= n -> a -> m a
+  go !m pLteEn !b = case Nat.monus m Nat.one of
+    Nothing -> pure b
+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+      let !cLtEn = descendLemma cPlusOneEqP pLteEn
+       in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b
 
--- | Monadic traversal of the numbers bounded by @n@
--- in descending order.
---
--- > descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0
-descendM_ :: forall m a n. Applicative m
-  => Nat n -- ^ Upper bound
-  -> (Fin n -> m a) -- ^ Effectful interpretion
-  -> m ()
-{-# inline descendM_ #-}
+{- | Monadic traversal of the numbers bounded by @n@
+in descending order.
+
+> descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0
+-}
+descendM_ ::
+  forall m a n.
+  (Applicative m) =>
+  -- | Upper bound
+  Nat n ->
+  -- | Effectful interpretion
+  (Fin n -> m a) ->
+  m ()
+{-# INLINE descendM_ #-}
 descendM_ !n f = go n Lte.reflexive
-  where
+ where
   go :: Nat p -> p <= n -> m ()
   go !m !pLteEn = case Nat.monus m Nat.one of
     Nothing -> pure ()
     Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
       let !cLtEn = descendLemma cPlusOneEqP pLteEn
-      in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn)
+       in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn)
 
--- | Generate all values of a finite set in ascending order.
---
--- >>> ascending (Nat.constant @3)
--- [Fin 0,Fin 1,Fin 2]
+{- | Generate all values of a finite set in ascending order.
+
+>>> ascending (Nat.constant @3)
+[Fin 0,Fin 1,Fin 2]
+-}
 ascending :: forall n. Nat n -> [Fin n]
 ascending !n = go Nat.zero
-  where
+ where
   go :: Nat m -> [Fin n]
   go !m = case m <? n of
     Nothing -> []
     Just lt -> Fin m lt : go (Nat.succ m)
 
--- | Generate all values of a finite set in descending order.
---
--- >>> descending (Nat.constant @3)
--- [Fin 2,Fin 1,Fin 0]
+{- | Generate all values of a finite set in descending order.
+
+>>> descending (Nat.constant @3)
+[Fin 2,Fin 1,Fin 0]
+-}
 descending :: forall n. Nat n -> [Fin n]
 descending !n = go n Lte.reflexive
-  where
-    go :: Nat p -> (p <= n) -> [Fin n]
-    go !m !pLteEn = case Nat.monus m Nat.one of
-      Nothing -> []
-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
-        let !cLtEn = descendLemma cPlusOneEqP pLteEn
-        in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn)
+ where
+  go :: Nat p -> (p <= n) -> [Fin n]
+  go !m !pLteEn = case Nat.monus m Nat.one of
+    Nothing -> []
+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->
+      let !cLtEn = descendLemma cPlusOneEqP pLteEn
+       in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn)
 
--- | Generate 'len' values starting from 'off' in ascending order.
---
--- >>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)
--- [Fin 2,Fin 3,Fin 4]
-ascendingSlice
-  :: forall n off len
-  .  Nat off
-  -> Nat len
-  -> off + len <= n
-  -> [Fin n]
-{-# inline ascendingSlice #-}
+{- | Generate 'len' values starting from 'off' in ascending order.
+
+>>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)
+[Fin 2,Fin 3,Fin 4]
+-}
+ascendingSlice ::
+  forall n off len.
+  Nat off ->
+  Nat len ->
+  off + len <= n ->
+  [Fin n]
+{-# INLINE ascendingSlice #-}
 ascendingSlice off len !offPlusLenLteEn = go Nat.zero
-  where
-    go :: Nat m -> [Fin n]
-    go !m = case m <? len of
-      Nothing -> []
-      Just emLtLen ->
-        let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen
-            !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn
-         in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)
+ where
+  go :: Nat m -> [Fin n]
+  go !m = case m <? len of
+    Nothing -> []
+    Just emLtLen ->
+      let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen
+          !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn
+       in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)
 
--- | Generate 'len' values starting from 'off + len - 1' in descending order.
---
--- >>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
--- [Fin 4,Fin 3,Fin 2]
-descendingSlice
-  :: forall n off len
-  .  Nat off
-  -> Nat len
-  -> off + len <= n
-  -> [Fin n]
-{-# inline descendingSlice #-}
+{- | Generate 'len' values starting from 'off + len - 1' in descending order.
+
+>>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
+[Fin 4,Fin 3,Fin 2]
+-}
+descendingSlice ::
+  forall n off len.
+  Nat off ->
+  Nat len ->
+  off + len <= n ->
+  [Fin n]
+{-# INLINE descendingSlice #-}
 descendingSlice !off !len !offPlusLenLteEn =
   go len Lte.reflexive
-  where
-    go :: Nat m -> m <= len -> [Fin n]
-    go !m !mLteEn = case Nat.monus m Nat.one of
-      Nothing -> []
-      Just (Difference (mpred :: Nat c) cPlusOneEqEm) ->
-        let !cLtLen = Lt.transitiveNonstrictR
+ where
+  go :: Nat m -> m <= len -> [Fin n]
+  go !m !mLteEn = case Nat.monus m Nat.one of
+    Nothing -> []
+    Just (Difference (mpred :: Nat c) cPlusOneEqEm) ->
+      let !cLtLen =
+            Lt.transitiveNonstrictR
               (Lt.substituteR (Plus.commutative @1 @c) (Lt.plus Lt.zero Lte.reflexive))
               -- c < c + 1
               (Lte.substituteL (Eq.symmetric cPlusOneEqEm) mLteEn)
-              -- c + 1 <= len
-            !cPlusOffLtEn = Lt.transitiveNonstrictR
-              (Lt.substituteR
-                (Plus.commutative @len @off)
-                (Lt.plus cLtLen (Lte.reflexive @off)))
+          -- c + 1 <= len
+          !cPlusOffLtEn =
+            Lt.transitiveNonstrictR
+              ( Lt.substituteR
+                  (Plus.commutative @len @off)
+                  (Lt.plus cLtLen (Lte.reflexive @off))
+              )
               -- c + off < off + len
               offPlusLenLteEn
-        in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen)
+       in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen)
 
--- | Extract the 'Int' from a 'Fin n'. This is intended to be used
--- at a boundary where a safe interface meets the unsafe primitives
--- on top of which it is built.
+{- | Extract the 'Int' from a 'Fin n'. This is intended to be used
+at a boundary where a safe interface meets the unsafe primitives
+on top of which it is built.
+-}
 demote :: Fin n -> Int
-{-# inline demote #-}
+{-# INLINE demote #-}
 demote (Fin i _) = Nat.demote i
 
 demote# :: Fin# n -> Int#
-{-# inline demote# #-}
+{-# INLINE demote# #-}
 demote# (Fin# i) = i
 
 lift :: Unsafe.Fin# n -> Fin n
-{-# inline lift #-}
+{-# INLINE lift #-}
 lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt
 
 unlift :: Fin n -> Unsafe.Fin# n
-{-# inline unlift #-}
+{-# INLINE unlift #-}
 unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i
 
 -- | Consume the natural number and the proof in the Fin.
 with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a
-{-# inline with #-}
+{-# INLINE with #-}
 with (Fin i lt) f = f lt i
 
 -- | Variant of 'with' for unboxed argument and result types.
 with# :: Fin# n -> (forall i. (i <# n) -> Nat# i -> a) -> a
-{-# inline with# #-}
+{-# INLINE with# #-}
 with# (Unsafe.Fin# i) f = f (Unsafe.Lt# (# #)) (Unsafe.Nat# i)
 
 construct# :: (i <# n) -> Nat# i -> Fin# n
-{-# inline construct# #-}
+{-# INLINE construct# #-}
 construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x
 
--- | Return the successor of the Fin or return nothing if the
--- argument is the greatest inhabitant.
+{- | Return the successor of the Fin or return nothing if the
+argument is the greatest inhabitant.
+-}
 succ :: Nat n -> Fin n -> Maybe (Fin n)
-{-# inline succ #-}
+{-# INLINE succ #-}
 succ n (Fin ix _) = case ix' <? n of
   Nothing -> Nothing
   Just lt -> Just (Fin ix' lt)
-  where
+ where
   ix' = Nat.succ ix
 
 -- | Variant of 'succ' for unlifted finite numbers.
 succ# :: Nat# n -> Fin# n -> MaybeFin# n
-{-# inline succ# #-}
+{-# INLINE succ# #-}
 succ# (Nat# n) (Fin# ix) = case ix' Exts.<# n of
   0# -> MaybeFinNothing#
   _ -> MaybeFinJust# (Fin# ix')
-  where
+ where
   !ix' = ix +# 1#
 
--- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
--- the remainder.
+{- | Convert an Int to a finite number, testing that it is
+less than the upper bound. This crashes with an uncatchable
+exception when given a negative number.
+-}
+fromInt ::
+  -- | exclusive upper bound
+  Nat n ->
+  Int ->
+  Maybe (Fin n)
+{-# INLINE fromInt #-}
+fromInt bound i
+  | i < 0 = errorWithoutStackTrace "Arithmetic.Fin.fromInt: negative argument"
+  | otherwise = Nat.with i $ \number -> case number <? bound of
+      Just lt -> Just (Fin number lt)
+      Nothing -> Nothing
+
+-- | Unboxed variant of 'fromInt'.
+fromInt# ::
+  -- | exclusive upper bound
+  Nat# n ->
+  Int# ->
+  MaybeFin# n
+{-# INLINE fromInt# #-}
+fromInt# (Nat# n) i
+  | Exts.isTrue# (i Exts.<# 0#) =
+      errorWithoutStackTrace "Arithmetic.Fin.fromInt#: negative argument"
+  | Exts.isTrue# (i Exts.<# n) = MaybeFinJust# (Fin# i)
+  | otherwise = MaybeFinNothing#
+
+{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
+the remainder.
+-}
 remInt# :: Int# -> Nat# n -> Fin# n
 remInt# i (Nat# n) = case n of
   0# -> errorWithoutStackTrace "Arithmetic.Fin.remInt#: cannot divide by zero"
   _ -> Fin# (Exts.remInt# i n)
 
--- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
--- the remainder.
+{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes
+the remainder.
+-}
 remWord# :: Word# -> Nat# n -> Fin# n
 remWord# w (Nat# n) = case n of
   0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero"
diff --git a/src/Arithmetic/Lt.hs b/src/Arithmetic/Lt.hs
--- a/src/Arithmetic/Lt.hs
+++ b/src/Arithmetic/Lt.hs
@@ -1,29 +1,32 @@
-{-# language AllowAmbiguousTypes #-}
-{-# language DataKinds #-}
-{-# language ExplicitForAll #-}
-{-# language KindSignatures #-}
-{-# language MagicHash #-}
-{-# language UnboxedTuples #-}
-{-# language TypeFamilies #-}
-{-# language TypeOperators #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
 
 module Arithmetic.Lt
   ( -- * Special Inequalities
     zero
   , zero#
+
     -- * Substitution
   , substituteL
   , substituteR
+
     -- * Increment
   , incrementL
   , incrementL#
   , incrementR
   , incrementR#
+
     -- * Decrement
   , decrementL
   , decrementL#
   , decrementR
   , decrementR#
+
     -- * Weaken
   , weakenL
   , weakenL#
@@ -31,6 +34,7 @@
   , weakenR#
   , weakenLhsL#
   , weakenLhsR#
+
     -- * Composition
   , plus
   , plus#
@@ -40,202 +44,247 @@
   , transitiveNonstrictL#
   , transitiveNonstrictR
   , transitiveNonstrictR#
+
     -- * Multiplication and Division
   , reciprocalA
   , reciprocalB
+
     -- * Convert to Inequality
   , toLteL
   , toLteR
+
     -- * Absurdities
   , absurd
+
     -- * Integration with GHC solver
   , constant
   , constant#
+
     -- * Lift and Unlift
   , lift
   , unlift
   ) where
 
-import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))
-import Arithmetic.Unsafe (type (<=)(Lte))
-import Arithmetic.Unsafe (type (<#)(Lt#),type (<=#))
-import GHC.TypeNats (CmpNat,type (+))
+import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte), type (<=#))
+import GHC.TypeNats (CmpNat, type (+))
 
 import qualified GHC.TypeNats as GHC
 
 toLteR :: (a < b) -> (a + 1 <= b)
-{-# inline toLteR #-}
+{-# INLINE toLteR #-}
 toLteR Lt = Lte
 
 toLteL :: (a < b) -> (1 + a <= b)
-{-# inline toLteL #-}
+{-# INLINE toLteL #-}
 toLteL Lt = Lte
 
--- | Replace the left-hand side of a strict inequality
--- with an equal number.
+{- | Replace the left-hand side of a strict inequality
+with an equal number.
+-}
 substituteL :: (b :=: c) -> (b < a) -> (c < a)
-{-# inline substituteL #-}
+{-# INLINE substituteL #-}
 substituteL Eq Lt = Lt
 
--- | Replace the right-hand side of a strict inequality
--- with an equal number.
+{- | Replace the right-hand side of a strict inequality
+with an equal number.
+-}
 substituteR :: (b :=: c) -> (a < b) -> (a < c)
-{-# inline substituteR #-}
+{-# INLINE substituteR #-}
 substituteR Eq Lt = Lt
 
 -- | Add a strict inequality to a nonstrict inequality.
 plus :: (a < b) -> (c <= d) -> (a + c < b + d)
-{-# inline plus #-}
+{-# INLINE plus #-}
 plus Lt Lte = Lt
 
 plus# :: (a <# b) -> (c <=# d) -> (a + c <# b + d)
-{-# inline plus# #-}
+{-# INLINE plus# #-}
 plus# _ _ = Lt# (# #)
 
--- | Add a constant to the left-hand side of both sides of
--- the strict inequality.
-incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a < b) -> (c + a < c + b)
-{-# inline incrementL #-}
+{- | Add a constant to the left-hand side of both sides of
+the strict inequality.
+-}
+incrementL ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) ->
+  (c + a < c + b)
+{-# INLINE incrementL #-}
 incrementL Lt = Lt
 
-incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <# b) -> (c + a <# c + b)
-{-# inline incrementL# #-}
+incrementL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <# b) ->
+  (c + a <# c + b)
+{-# INLINE incrementL# #-}
 incrementL# _ = Lt# (# #)
 
--- | Add a constant to the right-hand side of both sides of
--- the strict inequality.
-incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a < b) -> (a + c < b + c)
-{-# inline incrementR #-}
+{- | Add a constant to the right-hand side of both sides of
+the strict inequality.
+-}
+incrementR ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) ->
+  (a + c < b + c)
+{-# INLINE incrementR #-}
 incrementR Lt = Lt
 
-incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <# b) -> (a + c <# b + c)
-{-# inline incrementR# #-}
+incrementR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <# b) ->
+  (a + c <# b + c)
+{-# INLINE incrementR# #-}
 incrementR# _ = Lt# (# #)
 
--- | Subtract a constant from the left-hand side of both sides of
--- the inequality. This is the opposite of 'incrementL'.
-decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (c + a < c + b) -> (a < b)
-{-# inline decrementL #-}
+{- | Subtract a constant from the left-hand side of both sides of
+the inequality. This is the opposite of 'incrementL'.
+-}
+decrementL ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (c + a < c + b) ->
+  (a < b)
+{-# INLINE decrementL #-}
 decrementL Lt = Lt
 
-decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  ((c + a) <# (c + b)) -> (a <# b)
-{-# inline decrementL# #-}
+decrementL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  ((c + a) <# (c + b)) ->
+  (a <# b)
+{-# INLINE decrementL# #-}
 decrementL# _ = Lt# (# #)
 
--- | Subtract a constant from the right-hand side of both sides of
--- the inequality. This is the opposite of 'incrementR'.
-decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a + c < b + c) -> (a < b)
-{-# inline decrementR #-}
+{- | Subtract a constant from the right-hand side of both sides of
+the inequality. This is the opposite of 'incrementR'.
+-}
+decrementR ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c < b + c) ->
+  (a < b)
+{-# INLINE decrementR #-}
 decrementR Lt = Lt
 
-decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a + c <# b + c) -> (a <# b)
-{-# inline decrementR# #-}
+decrementR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c <# b + c) ->
+  (a <# b)
+{-# INLINE decrementR# #-}
 decrementR# _ = Lt# (# #)
 
--- | Add a constant to the left-hand side of the right-hand side of
--- the strict inequality.
-weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a < b) -> (a < c + b)
-{-# inline weakenL #-}
+{- | Add a constant to the left-hand side of the right-hand side of
+the strict inequality.
+-}
+weakenL ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) ->
+  (a < c + b)
+{-# INLINE weakenL #-}
 weakenL Lt = Lt
 
-weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <# b) -> (a <# c + b)
-{-# inline weakenL# #-}
+weakenL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <# b) ->
+  (a <# c + b)
+{-# INLINE weakenL# #-}
 weakenL# _ = Lt# (# #)
 
-weakenLhsL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (c + a <# b) -> (a <# b)
-{-# inline weakenLhsL# #-}
+weakenLhsL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (c + a <# b) ->
+  (a <# b)
+{-# INLINE weakenLhsL# #-}
 weakenLhsL# _ = Lt# (# #)
 
-weakenLhsR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a + c <# b) -> (a <# b)
-{-# inline weakenLhsR# #-}
+weakenLhsR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c <# b) ->
+  (a <# b)
+{-# INLINE weakenLhsR# #-}
 weakenLhsR# _ = Lt# (# #)
 
--- | Add a constant to the right-hand side of the right-hand side of
--- the strict inequality.
-weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a < b) -> (a < b + c)
-{-# inline weakenR #-}
+{- | Add a constant to the right-hand side of the right-hand side of
+the strict inequality.
+-}
+weakenR ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a < b) ->
+  (a < b + c)
+{-# INLINE weakenR #-}
 weakenR Lt = Lt
 
-weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <# b) -> (a <# b + c)
-{-# inline weakenR# #-}
+weakenR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <# b) ->
+  (a <# b + c)
+{-# INLINE weakenR# #-}
 weakenR# _ = Lt# (# #)
 
 -- | Compose two strict inequalities using transitivity.
 transitive :: (a < b) -> (b < c) -> (a < c)
-{-# inline transitive #-}
+{-# INLINE transitive #-}
 transitive Lt Lt = Lt
 
 transitive# :: (a <# b) -> (b <# c) -> (a <# c)
-{-# inline transitive# #-}
+{-# INLINE transitive# #-}
 transitive# _ _ = Lt# (# #)
 
--- | Compose a strict inequality (the first argument) with a nonstrict
--- inequality (the second argument).
+{- | Compose a strict inequality (the first argument) with a nonstrict
+inequality (the second argument).
+-}
 transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c)
-{-# inline transitiveNonstrictR #-}
+{-# INLINE transitiveNonstrictR #-}
 transitiveNonstrictR Lt Lte = Lt
 
 transitiveNonstrictR# :: (a <# b) -> (b <=# c) -> (a <# c)
-{-# inline transitiveNonstrictR# #-}
+{-# INLINE transitiveNonstrictR# #-}
 transitiveNonstrictR# _ _ = Lt# (# #)
 
 transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)
-{-# inline transitiveNonstrictL #-}
+{-# INLINE transitiveNonstrictL #-}
 transitiveNonstrictL Lte Lt = Lt
 
 transitiveNonstrictL# :: (a <=# b) -> (b <# c) -> (a <# c)
-{-# inline transitiveNonstrictL# #-}
+{-# INLINE transitiveNonstrictL# #-}
 transitiveNonstrictL# _ _ = Lt# (# #)
 
 -- | Zero is less than one.
 zero :: 0 < 1
-{-# inline zero #-}
+{-# INLINE zero #-}
 zero = Lt
 
 zero# :: (# #) -> 0 <# 1
-{-# inline zero# #-}
+{-# INLINE zero# #-}
 zero# _ = Lt# (# #)
 
 -- | Nothing is less than zero.
 absurd :: n < 0 -> void
-{-# inline absurd #-}
+{-# INLINE absurd #-}
 absurd Lt = errorWithoutStackTrace "Arithmetic.Nat.absurd: n < 0"
 
--- | Use GHC's built-in type-level arithmetic to prove
--- that one number is less than another. The type-checker
--- only reduces 'CmpNat' if both arguments are constants.
+{- | Use GHC's built-in type-level arithmetic to prove
+that one number is less than another. The type-checker
+only reduces 'CmpNat' if both arguments are constants.
+-}
 constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b)
-{-# inline constant #-}
+{-# INLINE constant #-}
 constant = Lt
 
 constant# :: forall a b. (CmpNat a b ~ 'LT) => (# #) -> (a <# b)
-{-# inline constant# #-}
+{-# INLINE constant# #-}
 constant# _ = Lt# (# #)
 
 -- | Given that @m < n/p@, we know that @p*m < n@.
-reciprocalA :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).
-  (m < GHC.Div n p) -> (p GHC.* m) < n
-{-# inline reciprocalA #-}
+reciprocalA ::
+  forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).
+  (m < GHC.Div n p) ->
+  (p GHC.* m) < n
+{-# INLINE reciprocalA #-}
 reciprocalA _ = Lt
 
 -- | Given that @m < roundUp(n/p)@, we know that @p*m < n@.
-reciprocalB :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).
-  (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n
-{-# inline reciprocalB #-}
+reciprocalB ::
+  forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).
+  (m < GHC.Div (n GHC.- 1) p + 1) ->
+  (p GHC.* m) < n
+{-# INLINE reciprocalB #-}
 reciprocalB _ = Lt
 
 unlift :: (a < b) -> (a <# b)
diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs
--- a/src/Arithmetic/Lte.hs
+++ b/src/Arithmetic/Lte.hs
@@ -1,198 +1,237 @@
-{-# language DataKinds #-}
-{-# language ExplicitForAll #-}
-{-# language KindSignatures #-}
-{-# language MagicHash #-}
-{-# language TypeFamilies #-}
-{-# language TypeOperators #-}
-{-# language UnboxedTuples #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
 
 module Arithmetic.Lte
   ( -- * Special Inequalities
     zero
   , reflexive
   , reflexive#
+
     -- * Substitution
   , substituteL
   , substituteR
+
     -- * Increment
   , incrementL
   , incrementL#
   , incrementR
   , incrementR#
+
     -- * Decrement
   , decrementL
   , decrementL#
   , decrementR
   , decrementR#
+
     -- * Weaken
   , weakenL
   , weakenL#
   , weakenR
   , weakenR#
+
     -- * Composition
   , transitive
   , transitive#
   , plus
   , plus#
+
     -- * Convert Strict Inequality
   , fromStrict
   , fromStrict#
   , fromStrictSucc
   , fromStrictSucc#
+
     -- * Integration with GHC solver
   , constant
+
     -- * Lift and Unlift
   , lift
   , unlift
   ) where
 
-import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))
-import Arithmetic.Unsafe (type (<=)(Lte))
-import Arithmetic.Unsafe (type (<=#)(Lte#),type (<#))
-import GHC.TypeNats (CmpNat,type (+))
+import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#), type (<=) (Lte), type (<=#) (Lte#))
+import GHC.TypeNats (CmpNat, type (+))
 
 import qualified GHC.TypeNats as GHC
 
--- | Replace the left-hand side of a strict inequality
--- with an equal number.
+{- | Replace the left-hand side of a strict inequality
+with an equal number.
+-}
 substituteL :: (b :=: c) -> (b <= a) -> (c <= a)
-{-# inline substituteL #-}
+{-# INLINE substituteL #-}
 substituteL Eq Lte = Lte
 
--- | Replace the right-hand side of a strict inequality
--- with an equal number.
+{- | Replace the right-hand side of a strict inequality
+with an equal number.
+-}
 substituteR :: (b :=: c) -> (a <= b) -> (a <= c)
-{-# inline substituteR #-}
+{-# INLINE substituteR #-}
 substituteR Eq Lte = Lte
 
 -- | Add two inequalities.
 plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)
-{-# inline plus #-}
+{-# INLINE plus #-}
 plus Lte Lte = Lte
 
 plus# :: (a <=# b) -> (c <=# d) -> (a + c <=# b + d)
-{-# inline plus# #-}
+{-# INLINE plus# #-}
 plus# _ _ = Lte# (# #)
 
 -- | Compose two inequalities using transitivity.
 transitive :: (a <= b) -> (b <= c) -> (a <= c)
-{-# inline transitive #-}
+{-# INLINE transitive #-}
 transitive Lte Lte = Lte
 
 transitive# :: (a <=# b) -> (b <=# c) -> (a <=# c)
-{-# inline transitive# #-}
+{-# INLINE transitive# #-}
 transitive# _ _ = Lte# (# #)
 
 -- | Any number is less-than-or-equal-to itself.
 reflexive :: a <= a
-{-# inline reflexive #-}
+{-# INLINE reflexive #-}
 reflexive = Lte
 
 reflexive# :: (# #) -> a <=# a
-{-# inline reflexive# #-}
+{-# INLINE reflexive# #-}
 reflexive# _ = Lte# (# #)
 
--- | Add a constant to the left-hand side of both sides of
--- the inequality.
-incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <= b) -> (c + a <= c + b)
-{-# inline incrementL #-}
+{- | Add a constant to the left-hand side of both sides of
+the inequality.
+-}
+incrementL ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) ->
+  (c + a <= c + b)
+{-# INLINE incrementL #-}
 incrementL Lte = Lte
 
-incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <=# b) -> (c + a <=# c + b)
-{-# inline incrementL# #-}
+incrementL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <=# b) ->
+  (c + a <=# c + b)
+{-# INLINE incrementL# #-}
 incrementL# _ = Lte# (# #)
 
--- | Add a constant to the right-hand side of both sides of
--- the inequality.
-incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <= b) -> (a + c <= b + c)
-{-# inline incrementR #-}
+{- | Add a constant to the right-hand side of both sides of
+the inequality.
+-}
+incrementR ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) ->
+  (a + c <= b + c)
+{-# INLINE incrementR #-}
 incrementR Lte = Lte
 
-incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <=# b) -> (a + c <=# b + c)
-{-# inline incrementR# #-}
+incrementR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <=# b) ->
+  (a + c <=# b + c)
+{-# INLINE incrementR# #-}
 incrementR# _ = Lte# (# #)
 
--- | Add a constant to the left-hand side of the right-hand side of
--- the inequality.
-weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <= b) -> (a <= c + b)
-{-# inline weakenL #-}
+{- | Add a constant to the left-hand side of the right-hand side of
+the inequality.
+-}
+weakenL ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) ->
+  (a <= c + b)
+{-# INLINE weakenL #-}
 weakenL Lte = Lte
 
-weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <=# b) -> (a <=# c + b)
-{-# inline weakenL# #-}
+weakenL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <=# b) ->
+  (a <=# c + b)
+{-# INLINE weakenL# #-}
 weakenL# _ = Lte# (# #)
 
--- | Add a constant to the right-hand side of the right-hand side of
--- the inequality.
-weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <= b) -> (a <= b + c)
-{-# inline weakenR #-}
+{- | Add a constant to the right-hand side of the right-hand side of
+the inequality.
+-}
+weakenR ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <= b) ->
+  (a <= b + c)
+{-# INLINE weakenR #-}
 weakenR Lte = Lte
 
-weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a <=# b) -> (a <=# b + c)
-{-# inline weakenR# #-}
+weakenR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a <=# b) ->
+  (a <=# b + c)
+{-# INLINE weakenR# #-}
 weakenR# _ = Lte# (# #)
 
--- | Subtract a constant from the left-hand side of both sides of
--- the inequality. This is the opposite of 'incrementL'.
-decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (c + a <= c + b) -> (a <= b)
-{-# inline decrementL #-}
+{- | Subtract a constant from the left-hand side of both sides of
+the inequality. This is the opposite of 'incrementL'.
+-}
+decrementL ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (c + a <= c + b) ->
+  (a <= b)
+{-# INLINE decrementL #-}
 decrementL Lte = Lte
 
-decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (c + a <=# c + b) -> (a <=# b)
-{-# inline decrementL# #-}
+decrementL# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (c + a <=# c + b) ->
+  (a <=# b)
+{-# INLINE decrementL# #-}
 decrementL# _ = Lte# (# #)
 
--- | Subtract a constant from the right-hand side of both sides of
--- the inequality. This is the opposite of 'incrementR'.
-decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a + c <= b + c) -> (a <= b)
-{-# inline decrementR #-}
+{- | Subtract a constant from the right-hand side of both sides of
+the inequality. This is the opposite of 'incrementR'.
+-}
+decrementR ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c <= b + c) ->
+  (a <= b)
+{-# INLINE decrementR #-}
 decrementR Lte = Lte
 
-decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
-  (a + c <=# b + c) -> (a <=# b)
-{-# inline decrementR# #-}
+decrementR# ::
+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
+  (a + c <=# b + c) ->
+  (a <=# b)
+{-# INLINE decrementR# #-}
 decrementR# _ = Lte# (# #)
 
 -- | Weaken a strict inequality to a non-strict inequality.
 fromStrict :: (a < b) -> (a <= b)
-{-# inline fromStrict #-}
+{-# INLINE fromStrict #-}
 fromStrict Lt = Lte
 
 fromStrict# :: (a <# b) -> (a <=# b)
-{-# inline fromStrict# #-}
+{-# INLINE fromStrict# #-}
 fromStrict# _ = Lte# (# #)
 
--- | Weaken a strict inequality to a non-strict inequality, incrementing
--- the right-hand argument by one.
+{- | Weaken a strict inequality to a non-strict inequality, incrementing
+the right-hand argument by one.
+-}
 fromStrictSucc :: (a < b) -> (a + 1 <= b)
-{-# inline fromStrictSucc #-}
+{-# INLINE fromStrictSucc #-}
 fromStrictSucc Lt = Lte
 
 fromStrictSucc# :: (a <# b) -> (a + 1 <=# b)
-{-# inline fromStrictSucc# #-}
+{-# INLINE fromStrictSucc# #-}
 fromStrictSucc# _ = Lte# (# #)
 
 -- | Zero is less-than-or-equal-to any number.
 zero :: 0 <= a
-{-# inline zero #-}
+{-# INLINE zero #-}
 zero = Lte
 
--- | Use GHC's built-in type-level arithmetic to prove
--- that one number is less-than-or-equal-to another. The type-checker
--- only reduces 'CmpNat' if both arguments are constants.
+{- | Use GHC's built-in type-level arithmetic to prove
+that one number is less-than-or-equal-to another. The type-checker
+only reduces 'CmpNat' if both arguments are constants.
+-}
 constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b)
-{-# inline constant #-}
+{-# INLINE constant #-}
 constant = Lte
 
 type family IsLte (o :: Ordering) :: Bool where
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
--- a/src/Arithmetic/Nat.hs
+++ b/src/Arithmetic/Nat.hs
@@ -1,28 +1,31 @@
-{-# language DataKinds #-}
-{-# language ExplicitForAll #-}
-{-# language KindSignatures #-}
-{-# language MagicHash #-}
-{-# language PatternSynonyms #-}
-{-# language RankNTypes #-}
-{-# language ScopedTypeVariables #-}
-{-# language TypeOperators #-}
-{-# language UnboxedTuples #-}
-{-# language UnboxedSums #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
 
 module Arithmetic.Nat
   ( -- * Addition
     plus
   , plus#
+
     -- * Subtraction
   , monus
+
     -- * Division
   , divide
   , divideRoundingUp
+
     -- * Multiplication
   , times
+
     -- * Successor
   , succ
   , succ#
+
     -- * Compare
   , testEqual
   , testEqual#
@@ -35,6 +38,7 @@
   , (<?)
   , (<?#)
   , (<=?)
+
     -- * Constants
   , zero
   , one
@@ -42,9 +46,11 @@
   , three
   , constant
   , constant#
+
     -- * Unboxed Constants
   , zero#
   , one#
+
     -- * Unboxed Pattern Synonyms
   , pattern N0#
   , pattern N1#
@@ -64,6 +70,7 @@
   , pattern N1024#
   , pattern N2048#
   , pattern N4096#
+
     -- * Convert
   , demote
   , demote#
@@ -76,73 +83,77 @@
 import Prelude hiding (succ)
 
 import Arithmetic.Types
-import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte), (:=:#)(Eq#))
-import Arithmetic.Unsafe (Nat(Nat),Nat#(Nat#),type (<)(Lt),type (<#)(Lt#))
-import GHC.Exts (Proxy#,proxy#,(+#),(<#),Int#,(==#))
-import GHC.TypeNats (type (+),type (-),Div,KnownNat,natVal')
-import GHC.Int (Int(I#))
-import Data.Maybe.Void (MaybeVoid#, pattern JustVoid#, pattern NothingVoid#)
+import Arithmetic.Unsafe (Nat (Nat), Nat# (Nat#), (:=:) (Eq), (:=:#) (Eq#), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte))
 import Data.Either.Void (EitherVoid#, pattern LeftVoid#, pattern RightVoid#)
+import Data.Maybe.Void (MaybeVoid#, pattern JustVoid#, pattern NothingVoid#)
+import GHC.Exts (Int#, Proxy#, proxy#, (+#), (<#), (==#))
+import GHC.Int (Int (I#))
+import GHC.TypeNats (Div, KnownNat, natVal', type (+), type (-))
 
 import qualified GHC.TypeNats as GHC
 
 -- | Infix synonym of 'testLessThan'.
 (<?) :: Nat a -> Nat b -> Maybe (a < b)
-{-# inline (<?) #-}
+{-# INLINE (<?) #-}
 (<?) = testLessThan
 
 -- | Infix synonym of 'testLessThanEqual'.
 (<=?) :: Nat a -> Nat b -> Maybe (a <= b)
-{-# inline (<=?) #-}
+{-# INLINE (<=?) #-}
 (<=?) = testLessThanEqual
 
 -- | Infix synonym of 'testEqual'.
 (=?) :: Nat a -> Nat b -> Maybe (a :=: b)
-{-# inline (=?) #-}
+{-# INLINE (=?) #-}
 (=?) = testEqual
 
 (<?#) :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)
-{-# inline (<?#) #-}
+{-# INLINE (<?#) #-}
 (<?#) = testLessThan#
 
--- | Is the first argument strictly less than the second
--- argument?
+{- | Is the first argument strictly less than the second
+argument?
+-}
 testLessThan :: Nat a -> Nat b -> Maybe (a < b)
-{-# inline testLessThan #-}
-testLessThan (Nat x) (Nat y) = if x < y
-  then Just Lt
-  else Nothing
+{-# INLINE testLessThan #-}
+testLessThan (Nat x) (Nat y) =
+  if x < y
+    then Just Lt
+    else Nothing
 
 testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)
-{-# inline testLessThan# #-}
+{-# INLINE testLessThan# #-}
 testLessThan# (Nat# x) (Nat# y) = case x <# y of
   0# -> NothingVoid#
   _ -> JustVoid# (Lt# (# #))
 
--- | Is the first argument less-than-or-equal-to the second
--- argument?
+{- | Is the first argument less-than-or-equal-to the second
+argument?
+-}
 testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
-{-# inline testLessThanEqual #-}
-testLessThanEqual (Nat x) (Nat y) = if x <= y
-  then Just Lte
-  else Nothing
+{-# INLINE testLessThanEqual #-}
+testLessThanEqual (Nat x) (Nat y) =
+  if x <= y
+    then Just Lte
+    else Nothing
 
 -- | Are the two arguments equal to one another?
 testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
-{-# inline testEqual #-}
-testEqual (Nat x) (Nat y) = if x == y
-  then Just Eq
-  else Nothing
+{-# INLINE testEqual #-}
+testEqual (Nat x) (Nat y) =
+  if x == y
+    then Just Eq
+    else Nothing
 
 testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b)
-{-# inline testEqual# #-}
+{-# INLINE testEqual# #-}
 testEqual# (Nat# x) (Nat# y) = case x ==# y of
   0# -> NothingVoid#
   _ -> JustVoid# (Eq# (# #))
 
 -- | Is zero equal to this number or less than it?
 testZero :: Nat a -> Either (0 :=: a) (0 < a)
-{-# inline testZero #-}
+{-# INLINE testZero #-}
 testZero (Nat x) = case x of
   0 -> Left Eq
   _ -> Right Lt
@@ -154,22 +165,22 @@
 
 -- | Add two numbers.
 plus :: Nat a -> Nat b -> Nat (a + b)
-{-# inline plus #-}
+{-# INLINE plus #-}
 plus (Nat x) (Nat y) = Nat (x + y)
 
 -- | Variant of 'plus' for unboxed nats.
 plus# :: Nat# a -> Nat# b -> Nat# (a + b)
-{-# inline plus# #-}
+{-# INLINE plus# #-}
 plus# (Nat# x) (Nat# y) = Nat# (x +# y)
 
 -- | Divide two numbers. Rounds down (towards zero)
 divide :: Nat a -> Nat b -> Nat (Div a b)
-{-# inline divide #-}
+{-# INLINE divide #-}
 divide (Nat x) (Nat y) = Nat (div x y)
 
 -- | Divide two numbers. Rounds up (away from zero)
 divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1)
-{-# inline divideRoundingUp #-}
+{-# INLINE divideRoundingUp #-}
 divideRoundingUp (Nat x) (Nat y) =
   -- Implementation note. We must use div so that when x=0,
   -- the result is (-1) and not 0. Then when we add 1, we get 0.
@@ -177,55 +188,58 @@
 
 -- | Multiply two numbers.
 times :: Nat a -> Nat b -> Nat (a GHC.* b)
-{-# inline times #-}
+{-# INLINE times #-}
 times (Nat x) (Nat y) = Nat (x * y)
 
 -- | The successor of a number.
 succ :: Nat a -> Nat (a + 1)
-{-# inline succ #-}
+{-# INLINE succ #-}
 succ n = plus n one
 
 -- | Unlifted variant of 'succ'.
 succ# :: Nat# a -> Nat# (a + 1)
-{-# inline succ# #-}
+{-# INLINE succ# #-}
 succ# n = plus# n (one# (# #))
 
 -- | Subtract the second argument from the first argument.
 monus :: Nat a -> Nat b -> Maybe (Difference a b)
-{-# inline monus #-}
-monus (Nat a) (Nat b) = let c = a - b in if c >= 0
-  then Just (Difference (Nat c) Eq)
-  else Nothing
+{-# INLINE monus #-}
+monus (Nat a) (Nat b) =
+  let c = a - b
+   in if c >= 0
+        then Just (Difference (Nat c) Eq)
+        else Nothing
 
 -- | The number zero.
 zero :: Nat 0
-{-# inline zero #-}
+{-# INLINE zero #-}
 zero = Nat 0
 
 -- | The number one.
 one :: Nat 1
-{-# inline one #-}
+{-# INLINE one #-}
 one = Nat 1
 
 -- | The number two.
 two :: Nat 2
-{-# inline two #-}
+{-# INLINE two #-}
 two = Nat 2
 
 -- | The number three.
 three :: Nat 3
-{-# inline three #-}
+{-# INLINE three #-}
 three = Nat 3
 
--- | Use GHC's built-in type-level arithmetic to create a witness
--- of a type-level number. This only reduces if the number is a
--- constant.
-constant :: forall n. KnownNat n => Nat n
-{-# inline constant #-}
+{- | Use GHC's built-in type-level arithmetic to create a witness
+of a type-level number. This only reduces if the number is a
+constant.
+-}
+constant :: forall n. (KnownNat n) => Nat n
+{-# INLINE constant #-}
 constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n)))
 
-constant# :: forall n. KnownNat n => (# #) -> Nat# n
-{-# inline constant# #-}
+constant# :: forall n. (KnownNat n) => (# #) -> Nat# n
+{-# INLINE constant# #-}
 constant# _ = case fromIntegral (natVal' (proxy# :: Proxy# n)) of
   I# i -> Nat# i
 
@@ -237,35 +251,37 @@
 one# :: (# #) -> Nat# 1
 one# _ = Nat# 1#
 
--- | Extract the 'Int' from a 'Nat'. This is intended to be used
--- at a boundary where a safe interface meets the unsafe primitives
--- on top of which it is built.
+{- | Extract the 'Int' from a 'Nat'. This is intended to be used
+at a boundary where a safe interface meets the unsafe primitives
+on top of which it is built.
+-}
 demote :: Nat n -> Int
-{-# inline demote #-}
+{-# INLINE demote #-}
 demote (Nat n) = n
 
 demote# :: Nat# n -> Int#
-{-# inline demote# #-}
+{-# INLINE demote# #-}
 demote# (Nat# n) = n
 
--- | Run a computation on a witness of a type-level number. The
--- argument 'Int' must be greater than or equal to zero. This is
--- not checked. Failure to upload this invariant will lead to a
--- segfault.
+{- | Run a computation on a witness of a type-level number. The
+argument 'Int' must be greater than or equal to zero. This is
+not checked. Failure to upload this invariant will lead to a
+segfault.
+-}
 with :: Int -> (forall n. Nat n -> a) -> a
-{-# inline with #-}
+{-# INLINE with #-}
 with i f = f (Nat i)
 
 with# :: Int# -> (forall n. Nat# n -> a) -> a
-{-# inline with# #-}
+{-# INLINE with# #-}
 with# i f = f (Nat# i)
 
 unlift :: Nat n -> Nat# n
-{-# inline unlift #-}
+{-# INLINE unlift #-}
 unlift (Nat (I# i)) = Nat# i
 
 lift :: Nat# n -> Nat n
-{-# inline lift #-}
+{-# INLINE lift #-}
 lift (Nat# i) = Nat (I# i)
 
 pattern N0# :: Nat# 0
diff --git a/src/Arithmetic/Plus.hs b/src/Arithmetic/Plus.hs
--- a/src/Arithmetic/Plus.hs
+++ b/src/Arithmetic/Plus.hs
@@ -1,8 +1,8 @@
-{-# language DataKinds #-}
-{-# language TypeOperators #-}
-{-# language KindSignatures #-}
-{-# language ExplicitForAll #-}
-{-# language AllowAmbiguousTypes #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Arithmetic.Plus
   ( zeroL
@@ -11,7 +11,7 @@
   , associative
   ) where
 
-import Arithmetic.Unsafe (type (:=:)(Eq))
+import Arithmetic.Unsafe (type (:=:) (Eq))
 import GHC.TypeNats (type (+))
 
 -- | Any number plus zero is equal to the original number.
diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs
--- a/src/Arithmetic/Types.hs
+++ b/src/Arithmetic/Types.hs
@@ -1,27 +1,27 @@
-{-# language DataKinds #-}
-{-# language MagicHash #-}
-{-# language ExplicitNamespaces #-}
-{-# language PatternSynonyms #-}
-{-# language ViewPatterns #-}
-{-# language GADTs #-}
-{-# language KindSignatures #-}
-{-# language RankNTypes #-}
-{-# language TypeOperators #-}
-{-# language UnboxedTuples #-}
-{-# language UnboxedSums #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Arithmetic.Types
   ( Nat
   , Nat#
-  , WithNat(..)
-  , Difference(..)
-  , Fin(..)
+  , WithNat (..)
+  , Difference (..)
+  , Fin (..)
   , Fin#
   , Fin32#
+
     -- * Maybe Fin
   , MaybeFin#
   , pattern MaybeFinJust#
   , pattern MaybeFinNothing#
+
     -- * Infix Operators
   , type (<)
   , type (<=)
@@ -31,11 +31,7 @@
   , type (:=:#)
   ) where
 
-import Arithmetic.Unsafe (Fin#(Fin#),Nat#,Nat(getNat), type (<=))
-import Arithmetic.Unsafe (Fin32#)
-import Arithmetic.Unsafe (MaybeFin#(..))
-import Arithmetic.Unsafe (type (<), type (:=:))
-import Arithmetic.Unsafe (type (<#), type (<=#), (:=:#))
+import Arithmetic.Unsafe (Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#))
 import Data.Kind (type Type)
 import GHC.TypeNats (type (+))
 
@@ -43,19 +39,22 @@
 
 data WithNat :: (GHC.Nat -> Type) -> Type where
   WithNat ::
-       {-# UNPACK #-} !(Nat n)
-    -> f n
-    -> WithNat f
+    {-# UNPACK #-} !(Nat n) ->
+    f n ->
+    WithNat f
 
 -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }'
 data Fin :: GHC.Nat -> Type where
-  Fin :: forall m n.
+  Fin ::
+    forall m n.
     { index :: !(Nat m)
     , proof :: !(m < n)
-    } -> Fin n
+    } ->
+    Fin n
 
--- | Proof that the first argument can be expressed as the
--- sum of the second argument and some other natural number.
+{- | Proof that the first argument can be expressed as the
+sum of the second argument and some other natural number.
+-}
 data Difference :: GHC.Nat -> GHC.Nat -> Type where
   -- It is safe for users of this library to use this data constructor
   -- freely. However, note that the interesting Difference values come
@@ -72,14 +71,15 @@
   Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)
 
 pattern MaybeFinJust# :: Fin# n -> MaybeFin# n
-pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #)) where
-  MaybeFinJust# (Fin# i) = MaybeFin# i
+pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #))
+  where
+    MaybeFinJust# (Fin# i) = MaybeFin# i
 
 pattern MaybeFinNothing# :: MaybeFin# n
 pattern MaybeFinNothing# = MaybeFin# (-1#)
 
 maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #)
-{-# inline maybeFinToFin# #-}
+{-# INLINE maybeFinToFin# #-}
 maybeFinToFin# (MaybeFin# i) = case i of
   -1# -> (# (# #) | #)
   _ -> (# | Fin# i #)
diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs
--- a/src/Arithmetic/Unsafe.hs
+++ b/src/Arithmetic/Unsafe.hs
@@ -1,35 +1,34 @@
-{-# language DataKinds #-}
-{-# language DerivingStrategies #-}
-{-# language ExplicitNamespaces #-}
-{-# language GADTSyntax #-}
-{-# language GeneralizedNewtypeDeriving #-}
-{-# language KindSignatures #-}
-{-# language MagicHash #-}
-{-# language RoleAnnotations #-}
-{-# language StandaloneDeriving #-}
-{-# language TypeOperators #-}
-{-# language UnboxedTuples #-}
-{-# language UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
 
 module Arithmetic.Unsafe
-  ( Nat(..)
-  , Nat#(..)
-  , Fin#(..)
-  , MaybeFin#(..)
-  , Fin32#(..)
-  , type (<#)(Lt#)
-  , type (<=#)(Lte#)
-  , type (<)(Lt)
-  , type (<=)(Lte)
-  , type (:=:)(Eq)
-  , type (:=:#)(Eq#)
+  ( Nat (..)
+  , Nat# (..)
+  , Fin# (..)
+  , MaybeFin# (..)
+  , Fin32# (..)
+  , type (<#) (Lt#)
+  , type (<=#) (Lte#)
+  , type (<) (Lt)
+  , type (<=) (Lte)
+  , type (:=:) (Eq)
+  , type (:=:#) (Eq#)
   ) where
 
-import Prelude hiding ((>=),(<=))
+import Prelude hiding ((<=), (>=))
 
 import Control.Category (Category)
 import Data.Kind (Type)
-import GHC.Exts (Int#,Int32#,TYPE,RuntimeRep(IntRep,Int32Rep,TupleRep))
+import GHC.Exts (Int#, Int32#, RuntimeRep (Int32Rep, IntRep, TupleRep), TYPE)
 
 import qualified Control.Category
 import qualified GHC.TypeNats as GHC
@@ -48,7 +47,8 @@
 infix 4 :=:#
 
 -- | A value-level representation of a natural number @n@.
-newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }
+newtype Nat (n :: GHC.Nat) = Nat {getNat :: Int}
+
 type role Nat nominal
 
 deriving newtype instance Show (Nat n)
@@ -56,34 +56,41 @@
 -- | Unboxed variant of Nat.
 newtype Nat# :: GHC.Nat -> TYPE 'IntRep where
   Nat# :: Int# -> Nat# n
+
 type role Nat# nominal
 
 -- | Finite numbers without the overhead of carrying around a proof.
 newtype Fin# :: GHC.Nat -> TYPE 'IntRep where
   Fin# :: Int# -> Fin# n
+
 type role Fin# nominal
 
--- | Either a @Fin#@ or Nothing. Internally, this uses negative
--- one to mean Nothing.
+{- | Either a @Fin#@ or Nothing. Internally, this uses negative
+one to mean Nothing.
+-}
 newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where
   MaybeFin# :: Int# -> MaybeFin# n
+
 type role MaybeFin# nominal
 
 -- | Variant of 'Fin#' that only allows 32-bit integers.
 newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where
   Fin32# :: Int32# -> Fin32# n
+
 type role Fin32# nominal
 
--- | Proof that the first argument is strictly less than the
--- second argument.
+{- | Proof that the first argument is strictly less than the
+second argument.
+-}
 data (<) :: GHC.Nat -> GHC.Nat -> Type where
   Lt :: a < b
 
 newtype (<#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where
   Lt# :: (# #) -> a <# b
 
--- | Proof that the first argument is less than or equal to the
--- second argument.
+{- | Proof that the first argument is less than or equal to the
+second argument.
+-}
 data (<=) :: GHC.Nat -> GHC.Nat -> Type where
   Lte :: a <= b