Safe Haskell	Safe
Language	Haskell2010

TypeFun.Data.Peano

Documentation

Constructors

Z
S N

Instances

Eq N Source #
Methods (==) :: N -> N -> Bool # (/=) :: N -> N -> Bool #
Ord N Source #
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 Source #
Methods readsPrec :: Int -> ReadS N # readList :: ReadS [N] # readPrec :: ReadPrec N # readListPrec :: ReadPrec [N] #
Show N Source #
Methods showsPrec :: Int -> N -> ShowS # show :: N -> String # showList :: [N] -> ShowS #
Generic N Source #
Associated Types type Rep N :: * -> * # Methods from :: N -> Rep N x # to :: Rep N x -> N #
type Rep N Source #
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 ... Source #

Equations

ToNat Z = 0
ToNat (S a) = 1 + ToNat a

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations