lens-5.0.1: Lenses, Folds and Traversals
Copyright (C) 2017 Edward Kmett
License BSD-style (see the file LICENSE)
Maintainer Edward Kmett <ekmett@gmail.com>
Stability provisional
Portability portable
Safe Haskell Safe-Inferred
Language Haskell2010

Numeric.Natural.Lens

Description

Useful tools for Gödel numbering.

Synopsis

Documentation

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

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

N = N*N

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

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

N = 2*N

_Naturals :: Iso' Natural [ Natural ] Source #

The natural numbers are isomorphic to lists of natural numbers

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

interleaves the bits of two natural numbers

pattern Sum :: Either Natural Natural -> Natural Source # 

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

pattern Naturals :: [ Natural ] -> Natural Source # 

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