Language.Symantic.Typing.Peano

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

Types Zero and Succ

data Zero

Instances

IPeano Zero

Defined in Language.Symantic.Typing.Peano

Methods

ipeano :: SPeano Zero

SymInjP Zero (Proxy s ': ss) (s :: k)

Defined in Language.Symantic.Compiling.Term

Methods

symInjP :: TeSym (Proxy s ': []) ts t -> TeSym (Proxy s ': ss) ts t

data Succ p

Instances

IPeano p => IPeano (Succ p)

Defined in Language.Symantic.Typing.Peano

Methods

ipeano :: SPeano (Succ p)

SymInjP p ss s => SymInjP (Succ p :: Type) (Proxy not_s ': ss) (s :: k2)

Defined in Language.Symantic.Compiling.Term

Methods

symInjP :: TeSym (Proxy s ': []) ts t -> TeSym (Proxy not_s ': ss) ts t

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

Defined in Language.Symantic.Typing.Peano

Methods

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

Type IPeano

class IPeano p where

Implicit construction of SPeano.

Methods

ipeano :: SPeano p

Instances

IPeano Zero

Defined in Language.Symantic.Typing.Peano

Methods

ipeano :: SPeano Zero

IPeano p => IPeano (Succ p)

Defined in Language.Symantic.Typing.Peano

Methods

ipeano :: SPeano (Succ p)

Type EPeano

data EPeano where

Constructors

EPeano :: SPeano p -> EPeano

Instances

Eq EPeano

Defined in Language.Symantic.Typing.Peano

Methods

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

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

Show EPeano

Defined in Language.Symantic.Typing.Peano

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