Documentation
a :#: b |
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' |
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 |
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) |
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 HAdd n1 n2 r | n1 n2 -> r whereSource
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
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) |