typical-0.0.1: Type level numbers, vectors, list. This lib needs to be extended.

Data.Typical

Documentation

data a :#: b Source

Constructors

a :#: b 

Instances

HMulSub HNil a (:#: a HNil) 
HAdd HNil HNil (:#: B0 HNil) 
HMergeBy f HNil (:#: a b) (:#: a b) 
HCompare HNil (:#: c d) HLT 
HMergeBy f (:#: a b) HNil (:#: a b) 
HAdd HNil b b' => HAdd HNil (:#: B1 b) (:#: B0 b') 
HAdd HNil (:#: B0 b) (:#: B1 b) 
HOrd HLT (:#: ha ta) (:#: hb tb) ha ta (:#: hb tb) 
HOrd HEQ (:#: ha ta) (:#: hb tb) ha ta (:#: hb tb) 
HOrd HGT (:#: ha ta) (:#: hb tb) hb (:#: ha ta) tb 
(HApply f (a, c) cmp, HOrd cmp (:#: a b) (:#: c d) h a' b', HMergeBy f a' b' e) => HMergeBy f (:#: a b) (:#: c d) (:#: h e) 
HNat a => HNat (:#: B1 a) 
HNat (:#: B1 HNil) 
HNat a => HNat (:#: B0 a) 
HDiv2 (:#: a b) b 
HTail (:#: a b) b 
HHead (:#: a b) a 
HCompare (:#: a b) HNil HGT 
HMulSub b (:#: B0 c) r => HMulSub (:#: B0 b) c r 
HSub (:#: B0 HNil) HNil HNil 
HMulSub b (:#: B0 c) r => HMulSub (:#: B1 b) c (:#: c r) 
HSub (:#: B1 b) HNil (:#: B0 b) 
HSub (:#: b c) HNil d => HSub (:#: B0 (:#: b c)) HNil (:#: B1 d) 
HAdd HNil a a' => HAdd (:#: B1 a) HNil (:#: B0 a') 
HAdd (:#: B0 a) HNil (:#: B1 a) 
HSplitAt (:#: a b) HNil (:#: a HNil) b 
(HCompare a c res1, HCompare b d res2, CalcRes res1 res2 res) => HCompare (:#: a b) (:#: c d) res 
HSub (:#: B1 HNil) (:#: B0 HNil) HNil 
HSub a b c => HSub (:#: B1 a) (:#: B1 b) (:#: B0 c) 
HSub (:#: a b) c d => HSub (:#: B1 (:#: a b)) (:#: B0 c) (:#: B1 d) 
(HAdd b N1 b', HSub a b' c) => HSub (:#: B0 a) (:#: B1 b) (:#: B1 c) 
HSub a b c => HSub (:#: B0 a) (:#: B0 b) (:#: B0 c) 
(HAdd a b c, HAdd HNil c c') => HAdd (:#: B1 a) (:#: B1 b) (:#: B0 c') 
HAdd a b c => HAdd (:#: B1 a) (:#: B0 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B1 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B0 b) (:#: B0 c) 
(HSub (:#: d d') HNil predD, HSplitAt b predD a' b') => HSplitAt (:#: a b) (:#: d d') (:#: a a') b' 

data HNil Source

Constructors

HNil 

Instances

HDiv2 HNil HNil 
HCompare HNil HNil HEQ 
HMergeBy f HNil HNil HNil 
HSplitAt HNil n HNil HNil 
HMulSub HNil a (:#: a HNil) 
HAdd HNil HNil (:#: B0 HNil) 
HMergeBy f HNil (:#: a b) (:#: a b) 
HCompare HNil (:#: c d) HLT 
HMergeBy f (:#: a b) HNil (:#: a b) 
HAdd HNil b b' => HAdd HNil (:#: B1 b) (:#: B0 b') 
HAdd HNil (:#: B0 b) (:#: B1 b) 
HNat (:#: B1 HNil) 
HCompare (:#: a b) HNil HGT 
HSub (:#: B0 HNil) HNil HNil 
HSub (:#: B1 b) HNil (:#: B0 b) 
HSub (:#: b c) HNil d => HSub (:#: B0 (:#: b c)) HNil (:#: B1 d) 
HAdd HNil a a' => HAdd (:#: B1 a) HNil (:#: B0 a') 
HAdd (:#: B0 a) HNil (:#: B1 a) 
HSplitAt (:#: a b) HNil (:#: a HNil) b 
HSub (:#: B1 HNil) (:#: B0 HNil) HNil 

class HHead a h | a -> h whereSource

Methods

hHead :: a -> hSource

Instances

HHead (:#: a b) a 

class HTail a t | a -> t whereSource

Methods

hTail :: a -> tSource

Instances

HTail (:#: a b) b 

class HSplitAt a n h t | a n -> h t whereSource

Methods

hSplitAt :: a -> n -> (h, t)Source

Instances

HSplitAt HNil n HNil HNil 
HSplitAt (:#: a b) HNil (:#: a HNil) b 
(HSub (:#: d d') HNil predD, HSplitAt b predD a' b') => HSplitAt (:#: a b) (:#: d d') (:#: a a') b' 

class HMergeBy f a b c | f a b -> c whereSource

Methods

hMergeBy :: f -> a -> b -> cSource

Instances

HMergeBy f HNil HNil HNil 
HMergeBy f HNil (:#: a b) (:#: a b) 
HMergeBy f (:#: a b) HNil (:#: a b) 
(HApply f (a, c) cmp, HOrd cmp (:#: a b) (:#: c d) h a' b', HMergeBy f a' b' e) => HMergeBy f (:#: a b) (:#: c d) (:#: h e) 

class HApply f parameter result | f parameter -> result whereSource

Methods

hApply :: f -> parameter -> resultSource

Instances

HCompare a b cmp => HApply HCmpHNat (a, b) cmp 

data B0 Source

Constructors

B0 

Instances

HCompare B1 B0 HGT 
HCompare B0 B1 HLT 
HCompare B0 B0 HEQ 
HAdd HNil HNil (:#: B0 HNil) 
HAdd HNil b b' => HAdd HNil (:#: B1 b) (:#: B0 b') 
HAdd HNil (:#: B0 b) (:#: B1 b) 
HNat a => HNat (:#: B0 a) 
HMulSub b (:#: B0 c) r => HMulSub (:#: B0 b) c r 
HSub (:#: B0 HNil) HNil HNil 
HSub (:#: B1 b) HNil (:#: B0 b) 
HSub (:#: b c) HNil d => HSub (:#: B0 (:#: b c)) HNil (:#: B1 d) 
HAdd HNil a a' => HAdd (:#: B1 a) HNil (:#: B0 a') 
HAdd (:#: B0 a) HNil (:#: B1 a) 
HSub (:#: B1 HNil) (:#: B0 HNil) HNil 
HSub a b c => HSub (:#: B1 a) (:#: B1 b) (:#: B0 c) 
HSub (:#: a b) c d => HSub (:#: B1 (:#: a b)) (:#: B0 c) (:#: B1 d) 
(HAdd b N1 b', HSub a b' c) => HSub (:#: B0 a) (:#: B1 b) (:#: B1 c) 
HSub a b c => HSub (:#: B0 a) (:#: B0 b) (:#: B0 c) 
(HAdd a b c, HAdd HNil c c') => HAdd (:#: B1 a) (:#: B1 b) (:#: B0 c') 
HAdd a b c => HAdd (:#: B1 a) (:#: B0 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B1 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B0 b) (:#: B0 c) 

data B1 Source

Constructors

B1 

Instances

HCompare B1 B1 HEQ 
HCompare B1 B0 HGT 
HCompare B0 B1 HLT 
HAdd HNil b b' => HAdd HNil (:#: B1 b) (:#: B0 b') 
HAdd HNil (:#: B0 b) (:#: B1 b) 
HNat a => HNat (:#: B1 a) 
HNat (:#: B1 HNil) 
HMulSub b (:#: B0 c) r => HMulSub (:#: B1 b) c (:#: c r) 
HSub (:#: B1 b) HNil (:#: B0 b) 
HSub (:#: b c) HNil d => HSub (:#: B0 (:#: b c)) HNil (:#: B1 d) 
HAdd HNil a a' => HAdd (:#: B1 a) HNil (:#: B0 a') 
HAdd (:#: B0 a) HNil (:#: B1 a) 
HSub (:#: B1 HNil) (:#: B0 HNil) HNil 
HSub a b c => HSub (:#: B1 a) (:#: B1 b) (:#: B0 c) 
HSub (:#: a b) c d => HSub (:#: B1 (:#: a b)) (:#: B0 c) (:#: B1 d) 
(HAdd b N1 b', HSub a b' c) => HSub (:#: B0 a) (:#: B1 b) (:#: B1 c) 
(HAdd a b c, HAdd HNil c c') => HAdd (:#: B1 a) (:#: B1 b) (:#: B0 c') 
HAdd a b c => HAdd (:#: B1 a) (:#: B0 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B1 b) (:#: B1 c) 

class HNat a Source

Instances

HNat a => HNat (:#: B1 a) 
HNat (:#: B1 HNil) 
HNat a => HNat (:#: B0 a) 

type N1 = HNilSource

type N4 = B0 :#: N2Source

class HAdd n1 n2 r | n1 n2 -> r whereSource

Methods

hAdd :: n1 -> n2 -> rSource

Instances

HAdd HNil HNil (:#: B0 HNil) 
HAdd HNil b b' => HAdd HNil (:#: B1 b) (:#: B0 b') 
HAdd HNil (:#: B0 b) (:#: B1 b) 
HAdd HNil a a' => HAdd (:#: B1 a) HNil (:#: B0 a') 
HAdd (:#: B0 a) HNil (:#: B1 a) 
(HAdd a b c, HAdd HNil c c') => HAdd (:#: B1 a) (:#: B1 b) (:#: B0 c') 
HAdd a b c => HAdd (:#: B1 a) (:#: B0 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B1 b) (:#: B1 c) 
HAdd a b c => HAdd (:#: B0 a) (:#: B0 b) (:#: B0 c) 

class HSub n1 n2 r | n1 n2 -> r whereSource

Methods

hSub :: n1 -> n2 -> rSource

Instances

HSub (:#: B0 HNil) HNil HNil 
HSub (:#: B1 b) HNil (:#: B0 b) 
HSub (:#: b c) HNil d => HSub (:#: B0 (:#: b c)) HNil (:#: B1 d) 
HSub (:#: B1 HNil) (:#: B0 HNil) HNil 
HSub a b c => HSub (:#: B1 a) (:#: B1 b) (:#: B0 c) 
HSub (:#: a b) c d => HSub (:#: B1 (:#: a b)) (:#: B0 c) (:#: B1 d) 
(HAdd b N1 b', HSub a b' c) => HSub (:#: B0 a) (:#: B1 b) (:#: B1 c) 
HSub a b c => HSub (:#: B0 a) (:#: B0 b) (:#: B0 c) 

class HMul a b c | a b -> c whereSource

Methods

hMul :: a -> b -> cSource

class HMulSub a b c | a b -> c whereSource

Methods

hMulSub :: a -> b -> cSource

Instances

HMulSub HNil a (:#: a HNil) 
HMulSub b (:#: B0 c) r => HMulSub (:#: B0 b) c r 
HMulSub b (:#: B0 c) r => HMulSub (:#: B1 b) c (:#: c r) 

class CalcRes a b c | a b -> c whereSource

Methods

calcRes :: a -> b -> cSource

class HOrd cmp a b h a' b' | cmp a b -> h a' b' whereSource

Methods

hOrd :: cmp -> a -> b -> (h, a', b')Source

Instances

HOrd HLT (:#: ha ta) (:#: hb tb) ha ta (:#: hb tb) 
HOrd HEQ (:#: ha ta) (:#: hb tb) ha ta (:#: hb tb) 
HOrd HGT (:#: ha ta) (:#: hb tb) hb (:#: ha ta) tb 

class HDiv2 a b | a -> b whereSource

Methods

hDiv2 :: a -> bSource

Instances

HDiv2 HNil HNil 
HDiv2 (:#: a b) b 

data HCmpHNat Source

Constructors

HCmpHNat 

Instances

HCompare a b cmp => HApply HCmpHNat (a, b) cmp