Language.Symantic.Typing.Peano

Natural numbers inductivey defined at the type-level, and of kind *.

Types Zero and Succ

data Zero

Instances

IPeano Zero

Methods

ipeano :: SPeano Zero

Inj_SymP k * Zero ((:) * (Proxy k s) ss) s

Methods

inj_SymP :: TeSym ((* ': Proxy Zero s) [*]) ts t -> TeSym ss ts t

data Succ p

Instances

Inj_SymP k * p ss s => Inj_SymP k * (Succ p) ((:) Type not_s ss) s

Methods

inj_SymP :: TeSym ((* ': Proxy (Succ p) s) [*]) ts t -> TeSym ss ts t

IPeano p => IPeano (Succ p)

Methods

ipeano :: SPeano (Succ p)

Type synonyms for a few numbers

type P0 = Zero

type P1 = Succ P0

type P2 = Succ P1

type P3 = Succ P2

Type SPeano

data SPeano p where

Singleton for Zero and Succ.

Constructors

SZero :: SPeano Zero

SSucc :: SPeano p -> SPeano (Succ p)

Instances

TestEquality * SPeano

Methods

testEquality :: f a -> f b -> Maybe ((SPeano :~: a) b)

Type IPeano

class IPeano p where

Implicit construction of SPeano.

Minimal complete definition

ipeano

Methods

ipeano :: SPeano p

Instances

IPeano Zero

Methods

ipeano :: SPeano Zero

IPeano p => IPeano (Succ p)

Methods

ipeano :: SPeano (Succ p)

Type EPeano

data EPeano where

Constructors

EPeano :: SPeano p -> EPeano

Instances

Eq EPeano

Methods

(==) :: EPeano -> EPeano -> Bool

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

Show EPeano

Methods

showsPrec :: Int -> EPeano -> ShowS

show :: EPeano -> String

showList :: [EPeano] -> ShowS

Interface with Integral

integral_from_peano :: Integral i => SPeano p -> i

peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret