type-fun-0.1.2: Collection of widely reimplemented type families

TypeFun.Data.Peano

data N Source #

Constructors

Defined in TypeFun.Data.Peano

Methods

(==) :: N -> N -> Bool #

(/=) :: N -> N -> Bool #

compare :: N -> N -> Ordering #

(<) :: N -> N -> Bool #

(<=) :: N -> N -> Bool #

(>) :: N -> N -> Bool #

(>=) :: N -> N -> Bool #

max :: N -> N -> N #

min :: N -> N -> N #

readsPrec :: Int -> ReadS N #

readList :: ReadS [N] #

readPrec :: ReadPrec N #

readListPrec :: ReadPrec [N] #

showsPrec :: Int -> N -> ShowS #

show :: N -> String #

showList :: [N] -> ShowS #

Associated Types

type Rep N :: Type -> Type #

from :: N -> Rep N x #

to :: Rep N x -> N #

class KnownPeano (p :: N) where Source #

Since: 0.1.2

peanoVal :: proxy p -> Integer Source #

peanoVal :: proxy Z -> Integer Source #

peanoVal :: proxy (S n) -> Integer Source #

type family ToNat (a :: N) :: Nat where ... Source #

Equations

type family FromNat (a :: Nat) :: N where ... Source #

type family (a :: N) :+: (b :: N) :: N where ... Source #

type family (a :: N) :-: (b :: N) :: N where ... Source #

type family (a :: N) :*: (b :: N) :: N where ... Source #