Documentation
Show HZero | |
HNat2Integral HZero | |
HNat HZero | |
HLength HNil HZero | |
HLt HZero HZero HFalse | |
HEq HZero HZero HTrue | |
HFind' HTrue e l HZero | |
HOccursNot e l => HType2HNatCase HTrue e l HZero | |
HUpdateAtHNat HZero e' (HCons e l) (HCons e' l) | |
HNat n => HLt HZero (HSucc n) HTrue | |
HNat n => HEq HZero (HSucc n) HFalse | |
HDeleteAtHNat HZero (HCons e l) l | |
HLookupByHNat HZero (HCons e l) e | |
Show (HSucc HZero) | |
HNat n => HLt (HSucc n) HZero HFalse | |
HNat n => HEq (HSucc n) HZero HFalse | |
HBetween (HSucc HZero) (HCons HZero HNil) |
HFind e l n => HFind' HFalse e l (HSucc n) | |
HType2HNat e l n => HType2HNatCase HFalse e l (HSucc n) | |
HNat n => HLt HZero (HSucc n) HTrue | |
HNat n => HEq HZero (HSucc n) HFalse | |
(HNat n, Show (HSucc n)) => Show (HSucc (HSucc n)) | |
Show (HSucc HZero) | |
HNat2Integral n => HNat2Integral (HSucc n) | |
HNat n => HNat (HSucc n) | |
(HNat x, HBetween (HSucc x) y, HAppend y (HCons (HSucc x) HNil) z, HList y) => HBetween (HSucc (HSucc x)) z | |
HNat n => HLt (HSucc n) HZero HFalse | |
HNat n => HEq (HSucc n) HZero HFalse | |
(HUpdateAtHNat n e' l l', HNat n) => HUpdateAtHNat (HSucc n) e' (HCons e l) (HCons e l') | |
(HNat n, HNat n', HLt n n' b) => HLt (HSucc n) (HSucc n') b | |
(HNat n, HNat n', HEq n n' b) => HEq (HSucc n) (HSucc n') b | |
HBetween (HSucc HZero) (HCons HZero HNil) | |
(HLookupByHNat n l e', HNat n) => HLookupByHNat (HSucc n) (HCons e l) e' | |
(HDeleteAtHNat n l l', HNat n) => HDeleteAtHNat (HSucc n) (HCons e l) (HCons e l') | |
(HLength l n, HNat n, HList l) => HLength (HCons a l) (HSucc n) |
class HNat n => HNat2Integral n whereSource
hNat2Integral :: Integral i => n -> iSource
HNat2Integral HZero | |
HNat2Integral n => HNat2Integral (HSucc n) |
Show HNothing | |
HMemberM e HNil HNothing | |
NarrowM'' f HNothing HNothing | |
HMemberM' HNothing e l HNothing | |
NarrowM' HNil rout b HNothing | |
H2ProjectByLabels ls r' rin rout => H2ProjectByLabels' HNothing ls (HCons f' r') rin (HCons f' rout) | |
FromHJust l l' => FromHJust (HCons HNothing l) l' | |
RecordEquiv' (r1 -> HNothing) pj2 HNothing | |
RecordEquiv' (r1 -> HJust r2) (r2 -> HNothing) HNothing |
HJust x |
NarrowM a HNil (HJust (Record HNil)) | |
HMemberM' HTrue e (HCons e l) (HJust l) | |
NarrowM'' f (HJust (Record r)) (HJust (Record (HCons f r))) | |
Show x => Show (HJust x) | |
HMemberM' (HJust l') e (HCons e' l) (HJust (HCons e' l')) | |
H2ProjectByLabels ls' r' rin rout => H2ProjectByLabels' (HJust ls') ls (HCons f' r') (HCons f' rin) rout | |
FromHJust l l' => FromHJust (HCons (HJust e) l) (HCons e l') | |
ToHJust l l' => ToHJust (HCons e l) (HCons (HJust e) l') | |
RecordEquiv' (r1 -> HJust r2) (r2 -> HNothing) HNothing | |
RecordEquiv' (r1 -> HJust r2) (r2 -> HJust r1) (HJust (r1 -> r2, r2 -> r1)) |
class HBool b => HEq x y b | x y -> bSource
TypeEq x y b => HEq x y b | |
HEq HZero HZero HTrue | |
HEq HNil HNil HTrue | |
HNat n => HEq HZero (HSucc n) HFalse | |
HList l => HEq HNil (HCons e l) HFalse | |
HNat n => HEq (HSucc n) HZero HFalse | |
TypeEq x y b => HEq (Proxy x) (Proxy y) b | |
(HNat n, HNat n', HEq n n' b) => HEq (HSucc n) (HSucc n') b | |
HEq n n' b => HEq (Label n) (Label n') b | |
HList l => HEq (HCons e l) HNil HFalse | |
(HList l, HList l', HEq e e' b, HEq l l' b', HAnd b b' b'') => HEq (HCons e l) (HCons e' l') b'' | |
HEq x x' b => HEq (Label x ns desc1) (Label x' ns desc2) b | |
(HEq x x' b, TypeEq ns ns' b', HAnd b b' b'') => HEq (Label x ns desc) (Label x' ns' desc') b'' |
Show (Proxy e) | |
Typeable x => Typeable (Proxy x) | |
Typeable x => ShowLabel (Proxy x) | |
TypeEq x y b => HEq (Proxy x) (Proxy y) b | |
HTypeProxied l => HTypeProxied (HCons (Proxy e) l) | |
Fail (ProxyFound x) => HasNoProxies (HCons (Proxy x) l) | |
Fail (ProxyFound x) => HasNoProxies (HCons (LVPair lab (Proxy x)) l) | |
(HType2HNat e l n, HTypes2HNats ps l ns) => HTypes2HNats (HCons (Proxy e) ps) l (HCons n ns) | |
HMaybied r r' => HMaybied (HCons (LVPair l (Proxy v)) r) (HCons (LVPair l (Maybe v)) r') |
class TypeEqTrue x y Source
TypeEqTrue x x |
class TypeEqFalse x y Source
TypeEqFalse x y | |
Fail () => TypeEqFalse x x |
typeEqTrue :: TypeEqTrue x y => x -> y -> ()Source
typeEqFalse :: TypeEqFalse x y => x -> y -> ()Source