Data.Type.Nat

Natural, Nat numbers

data Nat

toNatural

fromNatural

cata

Showing

explicitShow

explicitShowsPrec

Singleton

data SNat n

snatToNat

snatToNatural

Implicit

class SNatI n

reify

reflect

reflectToNum

Equality

eqNat

type family EqNat (n :: Nat) (m :: Nat) where ...

Induction

induction

induction1

class InlineInduction n

inlineInduction

Example: unfoldedFix

unfoldedFix

Arithmetic

type family Plus (n :: Nat) (m :: Nat) :: Nat where ...

type family Mult (n :: Nat) (m :: Nat) :: Nat where ...

Conversion to GHC Nat

type family ToGHC (n :: Nat) :: Nat where ...

type family FromGHC (n :: Nat) :: Nat where ...

Aliases

Nat

nat0

nat1

nat2

nat3

nat4

nat5

nat6

nat7

nat8

nat9

promoted Nat

type Nat0

type Nat1

type Nat2

type Nat3

type Nat4

type Nat5

type Nat6

type Nat7

type Nat8

type Nat9

Proofs

proofPlusZeroN

proofPlusNZero

proofMultZeroN

proofMultNZero

proofMultOneN

proofMultNOne