Data.HList.FakePrelude

Documentation

data HTrue

Instances

Show HTrue

HBool HTrue

TupleType () HTrue

TypeEq x x HTrue

HEq HZero HZero HTrue

HEq HNil HNil HTrue

HOr HFalse HTrue HTrue

HOr HTrue HFalse HTrue

HOr HTrue HTrue HTrue

HAnd HFalse HTrue HFalse

HAnd HTrue HFalse HFalse

HAnd HTrue HTrue HTrue

Eq e => HStagedEq' HTrue e e

Fail (DuplicatedLabel x) => HLabelSet' x ls HTrue

HCond HTrue x y x

HFind' HTrue e l HZero

HOccursNot e l => HType2HNatCase HTrue e l HZero

HLeftUnionBool HTrue r f r

HDeleteMany e l l' => HDeleteManyCase HTrue e e l l'

Fail (DuplicatedLabel l1) => HRLabelSet' l1 v1 l2 v2 HTrue r

HTIntersect t l1 l2 => HTIntersectBool HTrue h t l1 (HCons h l2)

(HList l, HOccursNot e l) => HOccursBool HTrue e (HCons e l)

HasField' HTrue l (HCons (LVPair l v) r) v

HasFieldP' HTrue l (RecordP (HCons l ls) (HCons v vs)) v

(UnionSymRec r1 r2' (Record ru), HasField l2 ru v2, HUpdateAtHNat n (LVPair l2 v2) ru ru, RecordLabels ru ls, HFind l2 ls n) => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru)

HMemberM' HTrue e (HCons e l) (HJust l)

H2ProjectByLabels ls (RecordP ls' vs') (RecordP lin vin) rout => H2ProjectByLabels' HTrue ls (RecordP (HCons l' ls') (HCons v' vs')) (RecordP (HCons l' lin) (HCons v' vin)) rout

HProjectByLabelP' HTrue l (HCons l ls) (HCons v vs) ls v vs

HNat n => HLt HZero (HSucc n) HTrue

TupleType (x, y) HTrue

HSplit l l' l'' => HSplit (HCons (e, HTrue) l) (HCons e l') l''

TupleType (x, y, z) HTrue

hTrue :: HTrue

data HFalse

Instances

Show HFalse

HBool HFalse

HLt HZero HZero HFalse

HOr HFalse HFalse HFalse

HOr HFalse HTrue HTrue

HOr HTrue HFalse HTrue

HAnd HFalse HFalse HFalse

HAnd HFalse HTrue HFalse

HAnd HTrue HFalse HFalse

HTMember e HNil HFalse

HMember e HNil HFalse

HStagedEq' HFalse e e'

HOrdMember e HNil HFalse

HLabelSet ls => HLabelSet' x ls HFalse

HCond HFalse x y y

TypeEq'' () x y HFalse

HTIntersect t l1 l2 => HTIntersectBool HFalse h t l1 l2

(HRLabelSet (HCons (LVPair l2 v2) r), HRLabelSet (HCons (LVPair l1 v1) r)) => HRLabelSet' l1 v1 l2 v2 HFalse r

(UnionSymRec r1 r2' (Record ru), HExtend f2 (Record ru) (Record (HCons f2 ru))) => UnionSymRec' HFalse r1 f2 r2' (Record (HCons f2 ru))

HDeleteMany e l l' => HDeleteManyCase HFalse e e' l (HCons e' l')

HFind e l n => HFind' HFalse e l (HSucc n)

HType2HNat e l n => HType2HNatCase HFalse e l (HSucc n)

HLeftUnionBool HFalse r f (HCons f r)

(HOccurs' e l, HList l) => HOccursBool HFalse e (HCons e' l)

(HMemberM e l r, HMemberM' r e (HCons e' l) res) => HMemberM' HFalse e (HCons e' l) res

HasField l r v => HasField' HFalse l (HCons fld r) v

HasField l (RecordP ls vs) v => HasFieldP' HFalse l (RecordP (HCons l' ls) (HCons v' vs)) v

H2ProjectByLabels ls (RecordP ls' vs') rin (RecordP lo vo) => H2ProjectByLabels' HFalse ls (RecordP (HCons l' ls') (HCons v' vs')) rin (RecordP (HCons l' lo) (HCons v' vo))

HProjectByLabelP l ls vs lso' v vso' => HProjectByLabelP' HFalse l (HCons l' ls) (HCons v' vs) (HCons l' lso') v (HCons v' vso')

HNat n => HEq HZero (HSucc n) HFalse

HList l => HEq HNil (HCons e l) HFalse

HNat n => HLt (HSucc n) HZero HFalse

HNat n => HEq (HSucc n) HZero HFalse

HList l => HEq (HCons e l) HNil HFalse

HSplit l l' l'' => HSplit (HCons (e, HFalse) l) l' (HCons e l'')

hFalse :: HFalse

class HBool x

Instances

HBool HFalse

HBool HTrue

class (HBool t, HBool t', HBool t'') => HAnd t t' t'' | t t' -> t'' where

Methods

hAnd :: t -> t' -> t''

Instances

HAnd HFalse HFalse HFalse

HAnd HFalse HTrue HFalse

HAnd HTrue HFalse HFalse

HAnd HTrue HTrue HTrue

class (HBool t, HBool t', HBool t'') => HOr t t' t'' | t t' -> t'' where

Methods

hOr :: t -> t' -> t''

Instances

HOr HFalse HFalse HFalse

HOr HFalse HTrue HTrue

HOr HTrue HFalse HTrue

HOr HTrue HTrue HTrue

class HBool t => HCond t x y z | t x y -> z where

Methods

hCond :: t -> x -> y -> z

Instances

HCond HFalse x y y

HCond HTrue x y x

data HZero

Instances

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)

data HSucc n

Instances

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)

hZero :: HZero

hSucc :: HNat n => n -> HSucc n

hPred :: HNat n => HSucc n -> n

class HNat n

Instances

HNat HZero

HNat n => HNat (HSucc n)

class HNat n => HNat2Integral n where

Methods

hNat2Integral :: Integral i => n -> i

Instances

HNat2Integral HZero

HNat2Integral n => HNat2Integral (HSucc n)

data HNothing

Constructors

HNothing

Instances

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

data HJust x

Constructors

HJust x

Instances

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 -> b

Instances

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''

hEq :: HEq x y b => x -> y -> b

class HStagedEq x y where

Methods

hStagedEq :: x -> y -> Bool

Instances

HStagedEq HNil HNil

HStagedEq HNil (HCons e l)

HStagedEq (HCons e l) HNil

(TypeEq e e' b, HStagedEq l l', HStagedEq' b e e') => HStagedEq (HCons e l) (HCons e' l')

class HBool b => HLt x y b | x y -> b

Instances

HLt HZero HZero HFalse

HNat n => HLt HZero (HSucc n) HTrue

HNat n => HLt (HSucc n) HZero HFalse

(HNat n, HNat n', HLt n n' b) => HLt (HSucc n) (HSucc n') b

hLt :: HLt x y b => x -> y -> b

class HBool b => TypeEq x y b | x y -> b

Instances

(HBool b, TypeCast HFalse b) => TypeEq x y b

TypeEq x x HTrue

typeEq :: TypeEq t t' b => t -> t' -> b

proxyEq :: TypeEq t t' b => Proxy t -> Proxy t' -> b

class TypeCast x y | x -> y, y -> x where

Methods

typeCast :: x -> y

Instances

TypeCast x x

data Proxy e

Instances

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')

proxy :: Proxy e

toProxy :: e -> Proxy e

unProxy :: Proxy e -> e

class TypeEqTrue x y

Instances

TypeEqTrue x x

class TypeEqFalse x y

Instances

TypeEqFalse x y

Fail () => TypeEqFalse x x

typeEqTrue :: TypeEqTrue x y => x -> y -> ()

typeEqFalse :: TypeEqFalse x y => x -> y -> ()

class SubType l l'

Instances

(HOccurs e l, SubType (TIP l) (TIP l')) => SubType (TIP l) (TIP (HCons e l'))

SubType (TIP l) (TIP HNil)

(RecordLabels r' ls, H2ProjectByLabels ls r r' rout) => SubType (Record r) (Record r')

H2ProjectByLabels ls' (RecordP ls vs) (RecordP ls' vs') rout => SubType (RecordP ls vs) (RecordP ls' vs')

subType :: SubType l l' => l -> l' -> ()

class Fail x