TypeFun.Data.Peano

Documentation

data N

Constructors

Z

S N

Instances

Eq N

Defined in TypeFun.Data.Peano

Methods

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

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

Ord N

Defined in TypeFun.Data.Peano

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

Defined in TypeFun.Data.Peano

Methods

readsPrec :: Int -> ReadS N

readList :: ReadS [N]

readPrec :: ReadPrec N

readListPrec :: ReadPrec [N]

Show N

Defined in TypeFun.Data.Peano

Methods

showsPrec :: Int -> N -> ShowS

show :: N -> String

showList :: [N] -> ShowS

Generic N

Defined in TypeFun.Data.Peano

Associated Types

type Rep N :: Type -> Type

Methods

from :: N -> Rep N x

to :: Rep N x -> N

type Rep N

Defined in TypeFun.Data.Peano

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

class KnownPeano (p :: N) where

Since: 0.1.2

Methods

peanoVal :: proxy p -> Integer

Instances

KnownPeano Z

Defined in TypeFun.Data.Peano

Methods

peanoVal :: proxy Z -> Integer

KnownPeano n => KnownPeano (S n)

Defined in TypeFun.Data.Peano

Methods

peanoVal :: proxy (S n) -> Integer

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)