HORIZON HASKELLDocslts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K
Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

Modulefin-0.3.2Haskell2010

Data.Nat

Nat numbers.

This module is designed to be imported qualified.

Contents
  1. Natural, Nat numbers
  2. Showing
  3. Aliases
Synopsis
  • Packagefin-0.3.2
  • Exports16
  • LanguageHaskell2010
  • LicenceBSD-3-Clause
  • SourceNat.hs

Natural, Nat numbers

datadata Nat
Source#

Nat natural numbers.

Better than GHC's built-in Nat for some use cases.

Constructors

Instances25Enum, Eq, Integral, Data, Num, Ord, …
  • Enum NatDefined in fin-0.3.2 · Data.Nat
  • Eq NatDefined in fin-0.3.2 · Data.Nat
  • Integral NatDefined in fin-0.3.2 · Data.Nat
  • Data NatDefined in fin-0.3.2 · Data.Nat
  • Num NatDefined in fin-0.3.2 · Data.Nat
  • Ord NatDefined in fin-0.3.2 · Data.Nat
  • Real NatDefined in fin-0.3.2 · Data.Nat
  • Show NatDefined in fin-0.3.2 · Data.Nat

    Nat is printed as Natural.

    To see explicit structure, use explicitShow or explicitShowsPrec

  • NFData NatDefined in fin-0.3.2 · Data.Nat
  • Arbitrary NatDefined in fin-0.3.2 · Data.Nat
  • CoArbitrary NatDefined in fin-0.3.2 · Data.Nat
  • Function NatDefined in fin-0.3.2 · Data.Nat
  • Hashable NatDefined in fin-0.3.2 · Data.Nat
  • Universe NatDefined in fin-0.3.2 · Data.Nat
    Example2 expressions
    import qualified Data.Universe.Class as Utake 10 (U.universe :: [Nat])[0,1,2,3,4,5,6,7,8,9]
  • Category LEProofDefined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep

    The other variant (Data.Type.Nat.LE.LEPRoof) isn't Category, because leRefl requires SNat evidence.

  • TestEquality SNatDefined in fin-0.3.2 · Data.Type.Nat
  • EqP FinDefined in fin-0.3.2 · Data.Fin
    Example1 expression
    eqp FZ FZTrue
    Example1 expression
    eqp FZ (FS FZ)False
    Example1 expression
    let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ][True,False,False,False,False,False][False,True,False,False,False,False][False,False,True,False,False,False][False,False,False,True,False,False]
  • EqP SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GCompare SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GEq SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GNFData SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GShow FinDefined in fin-0.3.2 · Data.Fin
  • GShow SNatDefined in fin-0.3.2 · Data.Type.Nat
  • OrdP FinDefined in fin-0.3.2 · Data.Fin
    Example1 expression
    let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ][EQ,LT,LT,LT,LT,LT][GT,EQ,LT,LT,LT,LT][GT,GT,EQ,LT,LT,LT][GT,GT,GT,EQ,LT,LT]
  • OrdP SNatDefined in fin-0.3.2 · Data.Type.Nat
valuetoNatural :: Nat -> Natural
Source#

Convert Nat to Natural

Example1 expression
toNatural 00
Example1 expression
toNatural 22
Example1 expression
toNatural $ S $ S $ Z2
valuecata :: a -> (a -> a) -> Nat -> a
Source#

Fold Nat.

Example1 expression
cata [] ('x' :) 2"xx"

Showing

Aliases