Safe Haskell	Safe-Inferred
Language	Haskell2010

TypeFun.Data.Peano

Synopsis

Documentation

Constructors

Z
S N

Instances details

Eq N Source #
Instance details Defined in TypeFun.Data.Peano Methods (==) :: N -> N -> Bool # (/=) :: N -> N -> Bool #
Ord N Source #
Instance details 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 Source #
Instance details Defined in TypeFun.Data.Peano Methods readsPrec :: Int -> ReadS N # readList :: ReadS [N] # readPrec :: ReadPrec N # readListPrec :: ReadPrec [N] #
Show N Source #
Instance details Defined in TypeFun.Data.Peano Methods showsPrec :: Int -> N -> ShowS # show :: N -> String # showList :: [N] -> ShowS #
Generic N Source #
Instance details 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 Source #
Instance details Defined in TypeFun.Data.Peano type Rep N = D1 ('MetaData "N" "TypeFun.Data.Peano" "type-fun-0.1.3-16uY0YJRvvj2DnEyZOrW5K" '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 Source #

Since: 0.1.2

Methods

Instances details

KnownPeano 'Z Source #
Instance details Defined in TypeFun.Data.Peano Methods peanoVal :: proxy 'Z -> Integer Source #
KnownPeano n => KnownPeano ('S n) Source #
Instance details Defined in TypeFun.Data.Peano Methods peanoVal :: proxy ('S n) -> Integer Source #

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