TypeFun.Data.Peano

Documentation

data N

Constructors

Z

S N

Instances

Eq N

Methods

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

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

Ord N

Methods

compare :: N -> N -> Ordering

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

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

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

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

max :: N -> N -> N

min :: N -> N -> N

Read N

Methods

readsPrec :: Int -> ReadS N

readList :: ReadS [N]

readPrec :: ReadPrec N

readListPrec :: ReadPrec [N]

Show N

Methods

showsPrec :: Int -> N -> ShowS

show :: N -> String

showList :: [N] -> ShowS

Generic N

Associated Types

type Rep N :: * -> *

Methods

from :: N -> Rep N x

to :: Rep N x -> N

type Rep N

type Rep N = D1 (MetaData "N" "TypeFun.Data.Peano" "type-fun-0.1.1-EXvG1zLdXJtBJ6ykEgIxfJ" False) ((:+:) (C1 (MetaCons "Z" PrefixI False) U1) (C1 (MetaCons "S" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 N))))

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

Equations

ToNat Z = 0

ToNat (S a) = 1 + ToNat a

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

Equations

FromNat 0 = Z

FromNat a = S (FromNat (a - 1))

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

Equations

Z :+: b = b

(S a) :+: b = a :+: S b

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

Equations

a :-: Z = a

(S a) :-: (S b) = a :-: b

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

Equations

Z :*: b = Z

a :*: Z = Z

(S a) :*: b = b :+: (a :*: b)