Documentation
class HNat n => HLookupByHNat n l e | n l -> e whereSource
hLookupByHNat :: n -> l -> eSource
HLookupByHNat HZero (HCons e l) e | |
(HLookupByHNat n l e', HNat n) => HLookupByHNat (HSucc n) (HCons e l) e' |
class HNat n => HDeleteAtHNat n l l' | n l -> l' whereSource
hDeleteAtHNat :: n -> l -> l'Source
HDeleteAtHNat HZero (HCons e l) l | |
(HDeleteAtHNat n l l', HNat n) => HDeleteAtHNat (HSucc n) (HCons e l) (HCons e l') |
class HNat n => HUpdateAtHNat n e l l' | n e l -> l', l' n -> e whereSource
hUpdateAtHNat :: n -> e -> l -> l'Source
HUpdateAtHNat HZero e' (HCons e l) (HCons e' l) | |
(HUpdateAtHNat n e' l l', HNat n) => HUpdateAtHNat (HSucc n) e' (HCons e l) (HCons e l') |
class HNats ns => HSplitByHNats' ns l l' l'' | ns l -> l' l'' whereSource
hSplitByHNats' :: ns -> l -> (l', l'')Source
HSplit l l' l'' => HSplitByHNats' HNil l HNil l' | |
(HLookupByHNat n l (e, b), HUpdateAtHNat n (e, HFalse) l l''', HSplitByHNats' ns l''' l' l'') => HSplitByHNats' (HCons n ns) l (HCons e l') l'' |
class HNats ns => HProjectByHNats ns l l' | ns l -> l' whereSource
hProjectByHNats :: ns -> l -> l'Source
HProjectByHNats HNil HNil HNil | |
HProjectByHNats HNil (HCons e l) HNil | |
(HLookupByHNat n (HCons e l) e', HProjectByHNats ns (HCons e l) l') => HProjectByHNats (HCons n ns) (HCons e l) (HCons e' l') |
class HProjectAwayByHNats ns l l' | ns l -> l' whereSource
hProjectAwayByHNats :: ns -> l -> l'Source
(HLength l len, HBetween len nats, HDiff nats ns ns', HProjectByHNats ns' l l') => HProjectAwayByHNats ns l l' |
class HOrdMember e l b | e l -> b whereSource
hOrdMember :: e -> l -> bSource
HOrdMember e HNil HFalse | |
(HEq e e' b1, HOrdMember e l b2, HOr b1 b2 b) => HOrdMember e (HCons e' l) b |
class HMaxLength l s Source
(HLength l s', HLt s' (HSucc s) HTrue) => HMaxLength l s |
class HMinLength l s Source
(HLength l s', HLt s (HSucc s') HTrue) => HMinLength l s |
class HSingleton l Source
HLength l (HSucc HZero) => HSingleton l |
hSingle :: (HSingleton l, HHead l e) => l -> eSource