lens-4.19.2: Lenses, Folds and Traversals
Copyright(C) 2017 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Numeric.Natural.Lens

Description

Useful tools for Gödel numbering.

Synopsis

Documentation

_Pair :: Iso' Natural (Natural, Natural) #

The natural numbers are isomorphic to the product of the natural numbers with itself.

N = N*N

_Sum :: Iso' Natural (Either Natural Natural) #

The natural numbers are isomorphic to disjoint sums of natural numbers embedded as evens or odds.

N = 2*N

_Naturals :: Iso' Natural [Natural] #

The natural numbers are isomorphic to lists of natural numbers

pattern Pair :: Natural -> Natural -> Natural #

interleaves the bits of two natural numbers

pattern Sum :: Either Natural Natural -> Natural #

Sum (Left q) = 2*q
Sum (Right q) = 2*q+1

pattern Naturals :: [Natural] -> Natural #

Naturals [] = 0
Naturals (h:t) = 1 + Pair h (Naturals t)