diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for lean-peano
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2020
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Author name here nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,1 @@
+# lean-peano
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE CPP #-}
+{-# OPTIONS_GHC -Wall #-}
+module Main (main) where
+
+import Distribution.Extra.Doctest ( defaultMainWithDoctests )
+main :: IO ()
+main = defaultMainWithDoctests "doctests"
diff --git a/doctest/doctests.hs b/doctest/doctests.hs
new file mode 100644
--- /dev/null
+++ b/doctest/doctests.hs
@@ -0,0 +1,14 @@
+module Main where
+
+import Build_doctests (flags, pkgs, module_sources)
+import Data.Foldable (traverse_)
+import System.Environment.Compat (unsetEnv)
+import Test.DocTest (doctest)
+
+main :: IO ()
+main = do
+    traverse_ putStrLn args
+    unsetEnv "GHC_ENVIRONMENT"
+    doctest args
+  where
+    args = flags ++ pkgs ++ module_sources
diff --git a/lean-peano.cabal b/lean-peano.cabal
new file mode 100644
--- /dev/null
+++ b/lean-peano.cabal
@@ -0,0 +1,73 @@
+cabal-version: >= 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 64e91e616abbba7139ad4f000d8a6a1505b2a315175f0489493a319d6a76ac89
+
+name:           lean-peano
+version:        0.1.0.0
+description:    Please see the README on GitHub at <https://github.com/githubuser/lean-peano#readme>
+homepage:       https://github.com/oisdk/lean-peano#readme
+bug-reports:    https://github.com/oisdk/lean-peano/issues
+author:         Donnacha Oisín Kidney
+maintainer:     mail@doisinkidney.com
+copyright:      2020 Donnacha Oisín Kidney
+license:        MIT
+license-file:   LICENSE
+build-type:     Custom
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/oisdk/lean-peano
+
+custom-setup
+  setup-depends:
+      base
+    , Cabal
+    , cabal-doctest  >=1.0.6 && <1.1
+
+library
+  exposed-modules:
+      Numeric.Peano
+      Numeric.Peano.Typelevel
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns -fwarn-redundant-constraints -Wcompat
+  build-depends:
+      base >=4.7 && <5
+    , deepseq
+  default-language: Haskell2010
+
+test-suite doctests
+  type: exitcode-stdio-1.0
+  main-is: doctests.hs
+  hs-source-dirs:
+      doctest
+  ghc-options: -Wall -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns -fwarn-redundant-constraints -Wcompat -threaded
+  build-depends:
+      QuickCheck
+    , base
+    , base-compat
+    , deepseq
+    , doctest
+    , lean-peano
+    , template-haskell
+  default-language: Haskell2010
+
+test-suite lean-peano-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns -fwarn-redundant-constraints -Wcompat -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base
+    , deepseq
+    , hedgehog
+    , lean-peano
+  default-language: Haskell2010
diff --git a/src/Numeric/Peano.hs b/src/Numeric/Peano.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Peano.hs
@@ -0,0 +1,246 @@
+{-# LANGUAGE BangPatterns         #-}
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE DeriveGeneric        #-}
+
+-- | Peano numerals. Effort is made to make them as efficient as
+-- possible, and as lazy as possible, but they are many orders of
+-- magnitude less efficient than machine integers. They are primarily
+-- used for type-level programming, and occasionally for calculations
+-- which can be short-circuited.
+--
+-- For instance, to check if two lists are the same length, you could
+-- write:
+--
+-- @
+-- 'length' xs == 'length' ys
+-- @
+--
+-- But this unnecessarily traverses both lists. The more efficient
+-- version, on the other hand, is less clear:
+--
+-- @
+-- sameLength [] [] = True
+-- sameLength (_:xs) (_:ys) = sameLength xs ys
+-- sameLength _ _ = False
+-- @
+--
+-- Using @'Data.List.genericLength'@, on the other hand, the laziness of
+-- @'Nat'@ will indeed short-circuit:
+--
+-- >>> genericLength [1,2,3] == genericLength [1..]
+-- False
+module Numeric.Peano where
+
+import           Data.List                   (unfoldr)
+
+import           Control.DeepSeq             (NFData (rnf))
+
+import           Data.Data                   (Data, Typeable)
+import           GHC.Generics                (Generic)
+
+import           Numeric.Natural
+
+import           Data.Ix
+
+import           Data.Function
+import           Text.Read
+
+-- $setup
+-- >>> import Test.QuickCheck
+-- >>> import Data.List (genericLength)
+-- >>> default (Nat)
+-- >>> :{
+-- instance Arbitrary Nat where
+--     arbitrary = fmap (fromInteger . getNonNegative) arbitrary
+-- :}
+
+-- | Peano numbers. Care is taken to make operations as lazy as
+-- possible:
+--
+-- >>> 1 > S (S undefined)
+-- False
+-- >>> Z > undefined
+-- False
+-- >>> 3 + undefined >= 3
+-- True
+data Nat
+    = Z
+    | S Nat
+    deriving (Eq,Generic,Data,Typeable)
+
+foldrNat :: (a -> a) -> a -> Nat -> a
+foldrNat f k = go
+  where
+    go Z     = k
+    go (S n) = f (go n)
+{-# INLINE foldrNat #-}
+
+foldlNat :: (a -> a) -> a -> Nat -> a
+foldlNat f = go
+  where
+    go !b Z = b
+    go !b (S n) = go (f b) n
+{-# INLINE foldlNat #-}
+
+-- | As lazy as possible
+instance Ord Nat where
+    compare Z Z         = EQ
+    compare (S n) (S m) = compare n m
+    compare Z (S _)     = LT
+    compare (S _) Z     = GT
+
+    Z   <= _   = True
+    S _ <= Z   = False
+    S n <= S m = n <= m
+
+    _ < Z = False
+    n < S m = n <= m
+
+    (>=) = flip (<=)
+    (>) = flip (<)
+
+    min Z _ = Z
+    min _ Z = Z
+    min (S n) (S m) = S (min n m)
+
+    max Z m = m
+    max n Z = n
+    max (S n) (S m) = S (max n m)
+
+-- | Subtraction stops at zero.
+--
+-- prop> n >= m ==> m - n == Z
+instance Num Nat where
+    n + m = foldrNat S m n
+    n * m = foldrNat (m+) Z n
+    abs = id
+    signum Z = Z
+    signum (S _) = S Z
+    fromInteger n
+        | n < 0 = error "cannot convert negative integers to Peano numbers"
+        | otherwise = go n where
+            go 0 = Z
+            go m = S (go (m-1))
+    n   - Z   = n
+    S n - S m = n - m
+    Z   - S _ = Z
+
+-- | The maximum bound here is infinity.
+--
+-- prop> maxBound > (n :: Nat)
+instance Bounded Nat where
+    minBound = Z
+    maxBound = fix S
+
+-- | Shows integer representation.
+instance Show Nat where
+    showsPrec n = showsPrec n . toInteger
+
+-- | Reads the integer representation.
+instance Read Nat where
+    readPrec = fmap (fromIntegral :: Natural -> Nat) readPrec
+
+-- | Will obviously diverge for values like `maxBound`.
+instance NFData Nat where
+    rnf Z     = ()
+    rnf (S n) = rnf n
+
+instance Real Nat where
+    toRational = toRational . toInteger
+
+-- | Uses custom 'enumFrom', 'enumFromThen', 'enumFromThenTo' to avoid
+-- expensive conversions to and from 'Int'.
+--
+-- >>> [1..3]
+-- [1,2,3]
+-- >>> [1..1]
+-- [1]
+-- >>> [2..1]
+-- []
+-- >>> take 3 [1,2..]
+-- [1,2,3]
+-- >>> take 3 [5,4..]
+-- [5,4,3]
+-- >>> [1,3..7]
+-- [1,3,5,7]
+-- >>> [5,4..1]
+-- [5,4,3,2,1]
+-- >>> [5,3..1]
+-- [5,3,1]
+instance Enum Nat where
+    succ = S
+    pred (S n) = n
+    pred Z = error "pred called on zero nat"
+    fromEnum = foldlNat succ 0
+    toEnum m
+      | m < 0 = error "cannot convert negative number to Peano"
+      | otherwise = go m
+      where
+        go 0 = Z
+        go n = S (go (n - 1))
+    enumFrom = iterate S
+    enumFromTo n m = unfoldr f (n, S m - n)
+      where
+        f (_,Z) = Nothing
+        f (e,S l) = Just (e, (S e, l))
+    enumFromThen n m = iterate t n
+      where
+        ts Z mm = (+) mm
+        ts (S nn) (S mm) = ts nn mm
+        ts nn Z = subtract nn
+        t = ts n m
+    enumFromThenTo n m t = unfoldr f (n, jm)
+      where
+        ts (S nn) (S mm) = ts nn mm
+        ts Z mm = (S t - n, (+) mm, mm)
+        ts nn Z = (S n - t, subtract nn, nn)
+        (jm,tf,tt) = ts n m
+        td = subtract tt
+        f (_,Z) = Nothing
+        f (e,l@(S _)) = Just (e, (tf e, td l))
+
+
+-- | Errors on zero.
+--
+-- >>> 5 `div` 2
+-- 2
+instance Integral Nat where
+    toInteger = foldlNat succ 0
+    quotRem _ Z = (maxBound, error "divide by zero")
+    quotRem x y = qr Z x y
+      where
+        qr q n m = go n m
+          where
+            go nn Z          = qr (S q) nn m
+            go (S nn) (S mm) = go nn mm
+            go Z (S _)       = (q, n)
+    quot n m = go n where
+      go = subt m where
+        subt Z nn          = S (go nn)
+        subt (S mm) (S nn) = subt mm nn
+        subt (S _) Z       = Z
+    rem _ Z = error "divide by zero"
+    rem nn mm = r nn mm where
+      r n m = go n m where
+        go nnn Z           = r nnn m
+        go (S nnn) (S mmm) = go nnn mmm
+        go Z (S _)         = n
+    div = quot
+    mod = rem
+    divMod = quotRem
+
+instance Ix Nat where
+    range = uncurry enumFromTo
+    inRange = uncurry go where
+      go (S _) _ Z         = False
+      go Z y x             = x <= y
+      go (S x) (S y) (S z) = go x y z
+      go (S _) Z (S _)     = False
+    index = uncurry go where
+      go Z h i             = lim 0 h i
+      go (S _) _ Z         = error "out of range"
+      go (S l) (S h) (S i) = go l h i
+      go (S _) Z (S _)     = error "out of range"
+      lim _ Z (S _)      = error "out of range"
+      lim !a (S n) (S m) = lim (a + 1) n m
+      lim !a _ Z         = a
diff --git a/src/Numeric/Peano/Typelevel.hs b/src/Numeric/Peano/Typelevel.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Peano/Typelevel.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE NoStarIsType         #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+module Numeric.Peano.Typelevel where
+
+import           GHC.TypeLits  (ErrorMessage (..), TypeError)
+import qualified GHC.TypeLits  as Lit
+import           Numeric.Peano
+
+type family (==) (n :: Nat) (m :: Nat) :: Bool where
+    Z == Z = True
+    S n == S m = n == m
+    Z == S _ = False
+    S _ == Z = False
+
+type family FromLit (n :: Lit.Nat) :: Nat where
+    FromLit 0 = Z
+    FromLit n = FromLit2 (Lit.Mod n 2) (FromLit (Lit.Div n 2))
+
+type family FromLit2 (odd :: Lit.Nat) (rest :: Nat) :: Nat where
+    FromLit2 0 n = n
+    FromLit2 1 n = S n
+
+type family ToLit (n :: Nat) :: Lit.Nat where
+    ToLit Z = 0
+    ToLit (S n) = 1 Lit.+ (ToLit n)
+
+type family Compare (n :: Nat) (m :: Nat) :: Ordering where
+    Compare Z Z         = EQ
+    Compare (S n) (S m) = Compare n m
+    Compare Z (S _)     = LT
+    Compare (S _) Z     = GT
+
+type family (<=) (n :: Nat) (m :: Nat) :: Bool where
+    Z   <= _   = True
+    S _ <= Z   = False
+    S n <= S m = n <= m
+
+type family (<) (n :: Nat) (m :: Nat) :: Bool where
+    _ < Z = False
+    n < S m = n <= m
+
+type family Min (n :: Nat) (m :: Nat) :: Nat where
+    Min Z _ = Z
+    Min _ Z = Z
+    Min (S n) (S m) = S (Min n m)
+
+type family Max (n :: Nat) (m :: Nat) :: Nat where
+    Max Z m = m
+    Max n Z = n
+    Max (S n) (S m) = S (Max n m)
+
+infixl 6 +
+type family (+) (n :: Nat) (m :: Nat) :: Nat where
+    Z + m = m
+    S n + m = S (n + m)
+
+infixl 7 *
+type family (*) (n :: Nat) (m :: Nat) :: Nat where
+    Z   * _ = Z
+    S n * m = m + n * m
+
+infixl 6 -
+type family (-) (n :: Nat) (m :: Nat) :: Nat where
+    n   - Z   = n
+    S n - S m = n - m
+    Z   - S _ = Z
+
+type family (%) (n :: Nat) (m :: Nat) :: Nat where
+    _ % Z = TypeError (Text "divide by zero")
+    n % m = Rem' n m n m
+
+type family Rem' (n :: Nat) (m :: Nat) (n' :: Nat) (m' :: Nat) :: Nat where
+    Rem' n m n' Z = Rem' n' m n' m
+    Rem' n m (S n') (S m') = Rem' n m n' m'
+    Rem' n m Z (S _) = n
+
+type family (/) (n :: Nat) (m :: Nat) :: Nat where
+    _ / Z = TypeError (Text "divide by zero")
+    n / m = Div' m n m
+
+type family Div' (m :: Nat) (n' :: Nat) (m' :: Nat) :: Nat where
+    Div' m n' Z = S (Div' m n' m)
+    Div' m (S n') (S m') = Div' m n' m'
+    Div' m Z (S _) = Z
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeApplications    #-}
+
+import           Hedgehog
+import qualified Hedgehog.Gen        as Gen
+import qualified Hedgehog.Range      as Range
+
+import           Numeric.Peano
+
+import           Control.Monad
+import           Data.Ix
+
+binaryProp
+    :: forall a.
+       Integral a
+    => (forall t. Integral t => t -> t -> t)
+    -> Integer
+    -> Integer
+    -> (Integer -> Integer -> Bool)
+    -> Property
+binaryProp op lb ub cond = property $ do
+    x <- forAll (Gen.integral (Range.linear lb ub))
+    y <- forAll (Gen.integral (Range.linear lb ub))
+    guard (cond x y)
+    let zb = op x y
+    let zt = op (fromInteger @a x) (fromInteger y)
+    zb === toInteger zt
+
+holdsForLength :: Foldable f => (a -> Bool) -> f a -> Int
+holdsForLength p = flip (foldr f id) 0 where
+  f e a i | p e = a (i + 1)
+          | otherwise = i
+
+enumProps
+    :: forall a.
+       (Enum a, Show a, Ord a)
+    => (Int -> Bool) -> Gen Int -> Gen a -> Property
+enumProps p ig eg = property $ do
+    x <- forAll ig
+    annotate "from . to"
+    (fromEnum . toEnum @a) x === x
+    annotate "to . from"
+    n <- forAll eg
+    (toEnum . fromEnum) n === n
+    annotate "[n..]"
+    let lhs1 = take 100 $ map fromEnum [n..]
+        rhs1 = take 100 [fromEnum n..]
+        len1 = min (holdsForLength p lhs1) (holdsForLength p rhs1)
+    take len1 lhs1 === take len1 rhs1
+    annotate "[n,m..]"
+    m <- forAll eg
+    let lhs2 = take 100 $ map fromEnum [n,m..]
+        rhs2 = take 100 [fromEnum n, fromEnum m..]
+        len2 = min (holdsForLength p lhs2) (holdsForLength p rhs2)
+    take len2 lhs2 === take len2 rhs2
+    when (m >= n) $ do
+        annotate "[n..m]"
+        map fromEnum [n..m] === [fromEnum n..fromEnum m]
+    l <- forAll eg
+    when (((l > n) == (n > m)) && (l /= n)) $ do
+        annotate "[l,n..m]"
+        map fromEnum [l,n..m] === [fromEnum l, fromEnum n..fromEnum m]
+
+
+prop_PeanoAdd :: Property
+prop_PeanoAdd = binaryProp @Nat (+) 0 1000 (\_ _ -> True)
+
+prop_PeanoMul :: Property
+prop_PeanoMul = binaryProp @Nat (*) 0 1000 (\_ _ -> True)
+
+prop_PeanoSub :: Property
+prop_PeanoSub = withDiscards 1000 $ binaryProp @Nat (-) 0 1000 (>=)
+
+prop_PeanoRem :: Property
+prop_PeanoRem = binaryProp @Nat rem 0 1000 (\_ y -> y > 0)
+
+prop_PeanoQuot :: Property
+prop_PeanoQuot = binaryProp @Nat quot 0 1000 (\_ y -> y > 0)
+
+-- prop_PeanoOrd :: Property
+-- prop_PeanoOrd = property $ ord (Gen.integral (Range.linear @Nat 0 1000))(\n -> Gen.integral (Range.linear n (n+5)))
+
+prop_PeanoEnum :: Property
+prop_PeanoEnum =
+    enumProps
+        (>= 0)
+        (Gen.integral (Range.linear 0 1000))
+        (Gen.integral (Range.linear @Nat 0 1000))
+
+prop_PeanoInRange :: Property
+prop_PeanoInRange = property $ do
+    l <- forAll (Gen.integral (Range.linear Z 100))
+    u <- forAll (Gen.integral (Range.linear l (l+100)))
+    i <- forAll (Gen.integral (Range.linear 0 300))
+    inRange (l,u) i === (l <= i &&  i <= u)
+
+prop_PeanoIndex :: Property
+prop_PeanoIndex = property $ do
+    l <- forAll (Gen.integral (Range.linear Z 100))
+    u <- forAll (Gen.integral (Range.linear l (l+100)))
+    i <- forAll (Gen.integral (Range.linear l u))
+    unless (inRange (l,u) i) discard
+    index (l,u) i === fromEnum (i - l)
+
+main :: IO Bool
+main = checkParallel $$(discover)