Portability	non-portable (FD and MPTC. empty data decls)
Stability	experimental
Maintainer	Edward Kmett <ekmett@gmail.com>
Safe Haskell	Safe-Infered

Data.Type.Boolean

Description

Simple closed type-level booleans.

Synopsis

Documentation

class TCBool Closure x => TBool x Source

...and every boolean is in that set. This lets us avoid carrying the closure parameter around

Instances

TBool F
TBool T

data F Source

Instances

Show F
TBool F
TBinary F
THex F
TNot F T
TNot T F
TCBool Closure F
Trichotomy F SignZero
TCBinary Closure F
TSucc T F
TSucc T F
TEven F T
TEven T F
Trichotomy F SignZero
THex2Binary' F F
TImplies F F T
TImplies F T T
TImplies T F F
TXOr' F F F
TXOr' F T T
TXOr' T F T
TXOr' T T F
TOr F F F
TOr F T T
TOr T F T
TAnd F F F
TAnd F T F
TAnd T F F
TLt TNothing TNothing F
TEq F F T
TEq F T F
TEq T F F
TEq Positive SignZero F
TEq Positive Negative F
TEq SignZero Positive F
TEq SignZero Negative F
TEq Negative Positive F
TEq Negative SignZero F
TCountBits' F F F
TShift' F F F
TShift' F T F
TShift' T F T
TMul a F F
TNF' F F F
TNF' T T F
LSB F F F
SHR1 H0 F F
TNF' F F F
TNF' T T F
LSN F H0 F	extract the least signficant nybble from a hex number
TMul a F F
TIf F x y y
TAddC' F F F F
TAddC' F T F T
TAddC' F T T F
TAddC' T F F T
TAddC' T F T F
TAddC' F F F F
TAddC' F T F T
TAddC' F T T F
TAddC' T F F T
TAddC' T F T F
TAddC' F F T (I F)
TAddC' T T F (O T)
TAddC' F F T (D1 F)
TAddC' T T F (DE T)
TPow a F (I F)
SHR1 H1 F (D1 F)
TPow' a F (D1 F)
TSucc F (I F)
TSucc F (D1 F)
TImplies F (I b) T
TImplies F (O b) T
TAnd F (I b) F
TAnd F (O b) F
TEq TNothing (TJust a) F
TSucc a b => TAddC' F (I a) T (O b)
TAddC' F (I a) F (I a)
TAddC' F (O a) T (I a)
TAddC' F (O a) F (O a)
TAddC' T (I a) F (O a)
TSucc b a => TAddC' T (O a) F (I b)
TSucc a b => TAddC' F (DF a) T (D0 b)
TAddC' F (DF a) F (DF a)
TAddC' F (DE a) F (DE a)
TAddC' F (DE a) T (DF a)
TAddC' F (DD a) F (DD a)
TAddC' F (DD a) T (DE a)
TAddC' F (DC a) F (DC a)
TAddC' F (DC a) T (DD a)
TAddC' F (DB a) F (DB a)
TAddC' F (DB a) T (DC a)
TAddC' F (DA a) F (DA a)
TAddC' F (DA a) T (DB a)
TAddC' F (D9 a) F (D9 a)
TAddC' F (D9 a) T (DA a)
TAddC' F (D8 a) F (D8 a)
TAddC' F (D8 a) T (D9 a)
TAddC' F (D7 a) F (D7 a)
TAddC' F (D7 a) T (D8 a)
TAddC' F (D6 a) F (D6 a)
TAddC' F (D6 a) T (D7 a)
TAddC' F (D5 a) F (D5 a)
TAddC' F (D5 a) T (D6 a)
TAddC' F (D4 a) F (D4 a)
TAddC' F (D4 a) T (D5 a)
TAddC' F (D3 a) F (D3 a)
TAddC' F (D3 a) T (D4 a)
TAddC' F (D2 a) F (D2 a)
TAddC' F (D2 a) T (D3 a)
TAddC' F (D1 a) F (D1 a)
TAddC' F (D1 a) T (D2 a)
TAddC' F (D0 a) F (D0 a)
TAddC' F (D0 a) T (D1 a)
TAddC' T (DF a) F (DE a)
TAddC' T (DE a) F (DD a)
TAddC' T (DD a) F (DC a)
TAddC' T (DC a) F (DB a)
TAddC' T (DB a) F (DA a)
TAddC' T (DA a) F (D9 a)
TAddC' T (D9 a) F (D8 a)
TAddC' T (D8 a) F (D7 a)
TAddC' T (D7 a) F (D6 a)
TAddC' T (D6 a) F (D5 a)
TAddC' T (D5 a) F (D4 a)
TAddC' T (D4 a) F (D3 a)
TAddC' T (D3 a) F (D2 a)
TAddC' T (D2 a) F (D1 a)
TAddC' T (D1 a) F (D0 a)
TSucc b a => TAddC' T (D0 a) F (DF b)
TXOr' F (I b) (I b)
TXOr' F (O b) (O b)
TOr F (I b) (I b)
TOr F (O b) (O b)
SHR1 H1 (DF F) (DF (D1 F))
SHR1 H1 (DE F) (DD (D1 F))
SHR1 H1 (DD F) (DB (D1 F))
SHR1 H1 (DC F) (D9 (D1 F))
SHR1 H1 (DB F) (D7 (D1 F))
SHR1 H1 (DA F) (D5 (D1 F))
SHR1 H1 (D9 F) (D3 (D1 F))
SHR1 H1 (D8 F) (D1 (D1 F))
SHR1 H1 (D7 F) (DF F)
SHR1 H1 (D6 F) (DD F)
SHR1 H1 (D5 F) (DB F)
SHR1 H1 (D4 F) (D9 F)
SHR1 H1 (D3 F) (D7 F)
SHR1 H1 (D2 F) (D5 F)
SHR1 H1 (D1 F) (D3 F)
SHR1 H1 (D0 F) (D1 F)
SHR1 H0 (DF F) (DE (D1 F))
SHR1 H0 (DE F) (DC (D1 F))
SHR1 H0 (DD F) (DA (D1 F))
SHR1 H0 (DC F) (D8 (D1 F))
SHR1 H0 (DB F) (D6 (D1 F))
SHR1 H0 (DA F) (D4 (D1 F))
SHR1 H0 (D9 F) (D2 (D1 F))
SHR1 H0 (D8 F) (D0 (D1 F))
SHR1 H0 (D7 F) (DE F)
SHR1 H0 (D6 F) (DC F)
SHR1 H0 (D5 F) (DA F)
SHR1 H0 (D4 F) (D8 F)
SHR1 H0 (D3 F) (D6 F)
SHR1 H0 (D2 F) (D4 F)
SHR1 H0 (D1 F) (D2 F)
SHR1 H0 (D0 F) (D0 F)
Trichotomy (I F) Positive
TEven (DF a) F
TEven (DD a) F
TEven (DB a) F
TEven (D9 a) F
TEven (D7 a) F
TEven (D5 a) F
TEven (D3 a) F
TEven (D1 a) F
Trichotomy (DF F) Positive
Trichotomy (DE F) Positive
Trichotomy (DD F) Positive
Trichotomy (DC F) Positive
Trichotomy (DB F) Positive
Trichotomy (DA F) Positive
Trichotomy (D9 F) Positive
Trichotomy (D8 F) Positive
Trichotomy (D7 F) Positive
Trichotomy (D6 F) Positive
Trichotomy (D5 F) Positive
Trichotomy (D4 F) Positive
Trichotomy (D3 F) Positive
Trichotomy (D2 F) Positive
Trichotomy (D1 F) Positive
TImplies (I a) F T
TImplies (O a) F T
TAnd (I a) F F
TAnd (O a) F F
TLt (TJust b) TNothing F
TEq (I m) F F
TEq (I m) T F
TEq (O m) T F
TEq (O m) F F
TEq (TJust a) TNothing F
(TCountBits' a n F, TSucc n m) => TCountBits' (I a) m F
TCountBits' a n F => TCountBits' (O a) n F
TNF' (I T) T F
TNF' (O F) F F
LSB (O a) F a => X (O a) F a
LSB (I F) T F
LSB (O T) F T
TNF' (DF T) T F
TNF' (D0 F) F F
LSN (DF F) HF F
LSN (DE F) HE F
LSN (DD F) HD F
LSN (DC F) HC F
LSN (DB F) HB F
LSN (DA F) HA F
LSN (D9 F) H9 F
LSN (D8 F) H8 F
LSN (D7 F) H7 F
LSN (D6 F) H6 F
LSN (D5 F) H5 F
LSN (D4 F) H4 F
LSN (D3 F) H3 F
LSN (D2 F) H2 F
LSN (D1 F) H1 F
TSucc a b => TAddC' (I a) F T (O b)
TAddC' (I a) T F (O a)
TAddC' (I a) F F (I a)
TSucc b a => TAddC' (O a) T F (I b)
TAddC' (O a) F T (I a)
TAddC' (O a) F F (O a)
TSucc a b => TAddC' (DF a) F T (D0 b)
TAddC' (DF a) F F (DF a)
TAddC' (DF a) T F (DE a)
TAddC' (DE a) F F (DE a)
TAddC' (DE a) F T (DF a)
TAddC' (DE a) T F (DD a)
TAddC' (DD a) F F (DD a)
TAddC' (DD a) F T (DE a)
TAddC' (DD a) T F (DC a)
TAddC' (DC a) F F (DC a)
TAddC' (DC a) F T (DD a)
TAddC' (DC a) T F (DB a)
TAddC' (DB a) F F (DB a)
TAddC' (DB a) F T (DC a)
TAddC' (DB a) T F (DA a)
TAddC' (DA a) F F (DA a)
TAddC' (DA a) F T (DB a)
TAddC' (DA a) T F (D9 a)
TAddC' (D9 a) F F (D9 a)
TAddC' (D9 a) F T (DA a)
TAddC' (D9 a) T F (D8 a)
TAddC' (D8 a) F F (D8 a)
TAddC' (D8 a) F T (D9 a)
TAddC' (D8 a) T F (D7 a)
TAddC' (D7 a) F F (D7 a)
TAddC' (D7 a) F T (D8 a)
TAddC' (D7 a) T F (D6 a)
TAddC' (D6 a) F F (D6 a)
TAddC' (D6 a) F T (D7 a)
TAddC' (D6 a) T F (D5 a)
TAddC' (D5 a) F F (D5 a)
TAddC' (D5 a) F T (D6 a)
TAddC' (D5 a) T F (D4 a)
TAddC' (D4 a) F F (D4 a)
TAddC' (D4 a) F T (D5 a)
TAddC' (D4 a) T F (D3 a)
TAddC' (D3 a) F F (D3 a)
TAddC' (D3 a) F T (D4 a)
TAddC' (D3 a) T F (D2 a)
TAddC' (D2 a) F F (D2 a)
TAddC' (D2 a) F T (D3 a)
TAddC' (D2 a) T F (D1 a)
TAddC' (D1 a) F F (D1 a)
TAddC' (D1 a) F T (D2 a)
TAddC' (D1 a) T F (D0 a)
TSucc b a => TAddC' (D0 a) T F (DF b)
TAddC' (D0 a) F F (D0 a)
TAddC' (D0 a) F T (D1 a)
TXOr' (I b) F (I b)
TXOr' (O b) F (O b)
TOr (I a) F (I a)
TOr (O a) F (I a)
TShift' (I a) F (I a)
TShift' (O a) F (O a)
LSB (O (I n)) F (I n)
LSB (O (O n)) F (O n)
TSucc (DE F) (DF F)
TSucc (DD F) (DE F)
TSucc (DC F) (DD F)
TSucc (DB F) (DC F)
TSucc (DA F) (DB F)
TSucc (D9 F) (DA F)
TSucc (D8 F) (D9 F)
TSucc (D7 F) (D8 F)
TSucc (D6 F) (D7 F)
TSucc (D5 F) (D6 F)
TSucc (D4 F) (D5 F)
TSucc (D3 F) (D4 F)
TSucc (D2 F) (D3 F)
TSucc (D1 F) (D2 F)
TEq (I m) (O n) F	Equality comparison. Note this does not equate numbers that are non-normalized with their normalized kin.
TEq (O m) (I n) F
TNF' (I F) (I F) T
TNF' (DF F) (DF F) T
TNF' (DE F) (DE F) T
TNF' (DD F) (DD F) T
TNF' (DC F) (DC F) T
TNF' (DB F) (DB F) T
TNF' (DA F) (DA F) T
TNF' (D9 F) (D9 F) T
TNF' (D8 F) (D8 F) T
TNF' (D7 F) (D7 F) T
TNF' (D6 F) (D6 F) T
TNF' (D5 F) (D5 F) T
TNF' (D4 F) (D4 F) T
TNF' (D3 F) (D3 F) T
TNF' (D2 F) (D2 F) T
TNF' (D1 F) (D1 F) T
TAddC' a b T c => TAddC' (I a) (I b) F (O c)
TAddC' a b F c => TAddC' (I a) (O b) F (I c)
TAddC' a b F c => TAddC' (O a) (I b) F (I c)
TAddC' a b F c => TAddC' (O a) (O b) F (O c)
TAddC' a b T c => TAddC' (DF a) (DF b) F (DE c)
TAddC' a b T c => TAddC' (DF a) (DE b) F (DD c)
TAddC' a b T c => TAddC' (DF a) (DD b) F (DC c)
TAddC' a b T c => TAddC' (DF a) (DC b) F (DB c)
TAddC' a b T c => TAddC' (DF a) (DB b) F (DA c)
TAddC' a b T c => TAddC' (DF a) (DA b) F (D9 c)
TAddC' a b T c => TAddC' (DF a) (D9 b) F (D8 c)
TAddC' a b T c => TAddC' (DF a) (D8 b) F (D7 c)
TAddC' a b T c => TAddC' (DF a) (D7 b) F (D6 c)
TAddC' a b T c => TAddC' (DF a) (D6 b) F (D5 c)
TAddC' a b T c => TAddC' (DF a) (D5 b) F (D4 c)
TAddC' a b T c => TAddC' (DF a) (D4 b) F (D3 c)
TAddC' a b T c => TAddC' (DF a) (D3 b) F (D2 c)
TAddC' a b T c => TAddC' (DF a) (D2 b) F (D1 c)
TAddC' a b T c => TAddC' (DF a) (D1 b) F (D0 c)
TAddC' a b F c => TAddC' (DF a) (D0 b) F (DF c)
TAddC' a b T c => TAddC' (DE a) (DF b) F (DD c)
TAddC' a b T c => TAddC' (DE a) (DE b) F (DC c)
TAddC' a b T c => TAddC' (DE a) (DD b) F (DB c)
TAddC' a b T c => TAddC' (DE a) (DC b) F (DA c)
TAddC' a b T c => TAddC' (DE a) (DB b) F (D9 c)
TAddC' a b T c => TAddC' (DE a) (DA b) F (D8 c)
TAddC' a b T c => TAddC' (DE a) (D9 b) F (D7 c)
TAddC' a b T c => TAddC' (DE a) (D8 b) F (D6 c)
TAddC' a b T c => TAddC' (DE a) (D7 b) F (D5 c)
TAddC' a b T c => TAddC' (DE a) (D6 b) F (D4 c)
TAddC' a b T c => TAddC' (DE a) (D5 b) F (D3 c)
TAddC' a b T c => TAddC' (DE a) (D4 b) F (D2 c)
TAddC' a b T c => TAddC' (DE a) (D3 b) F (D1 c)
TAddC' a b T c => TAddC' (DE a) (D2 b) F (D0 c)
TAddC' a b F c => TAddC' (DE a) (D1 b) F (DF c)
TAddC' a b F c => TAddC' (DE a) (D0 b) F (DE c)
TAddC' a b T c => TAddC' (DD a) (DF b) F (DC c)
TAddC' a b T c => TAddC' (DD a) (DE b) F (DB c)
TAddC' a b T c => TAddC' (DD a) (DD b) F (DA c)
TAddC' a b T c => TAddC' (DD a) (DC b) F (D9 c)
TAddC' a b T c => TAddC' (DD a) (DB b) F (D8 c)
TAddC' a b T c => TAddC' (DD a) (DA b) F (D7 c)
TAddC' a b T c => TAddC' (DD a) (D9 b) F (D6 c)
TAddC' a b T c => TAddC' (DD a) (D8 b) F (D5 c)
TAddC' a b T c => TAddC' (DD a) (D7 b) F (D4 c)
TAddC' a b T c => TAddC' (DD a) (D6 b) F (D3 c)
TAddC' a b T c => TAddC' (DD a) (D5 b) F (D2 c)
TAddC' a b T c => TAddC' (DD a) (D4 b) F (D1 c)
TAddC' a b T c => TAddC' (DD a) (D3 b) F (D0 c)
TAddC' a b F c => TAddC' (DD a) (D2 b) F (DF c)
TAddC' a b F c => TAddC' (DD a) (D1 b) F (DE c)
TAddC' a b F c => TAddC' (DD a) (D0 b) F (DD c)
TAddC' a b T c => TAddC' (DC a) (DF b) F (DB c)
TAddC' a b T c => TAddC' (DC a) (DE b) F (DA c)
TAddC' a b T c => TAddC' (DC a) (DD b) F (D9 c)
TAddC' a b T c => TAddC' (DC a) (DC b) F (D8 c)
TAddC' a b T c => TAddC' (DC a) (DB b) F (D7 c)
TAddC' a b T c => TAddC' (DC a) (DA b) F (D6 c)
TAddC' a b T c => TAddC' (DC a) (D9 b) F (D5 c)
TAddC' a b T c => TAddC' (DC a) (D8 b) F (D4 c)
TAddC' a b T c => TAddC' (DC a) (D7 b) F (D3 c)
TAddC' a b T c => TAddC' (DC a) (D6 b) F (D2 c)
TAddC' a b T c => TAddC' (DC a) (D5 b) F (D1 c)
TAddC' a b T c => TAddC' (DC a) (D4 b) F (D0 c)
TAddC' a b F c => TAddC' (DC a) (D3 b) F (DF c)
TAddC' a b F c => TAddC' (DC a) (D2 b) F (DE c)
TAddC' a b F c => TAddC' (DC a) (D1 b) F (DD c)
TAddC' a b F c => TAddC' (DC a) (D0 b) F (DC c)
TAddC' a b T c => TAddC' (DB a) (DF b) F (DA c)
TAddC' a b T c => TAddC' (DB a) (DE b) F (D9 c)
TAddC' a b T c => TAddC' (DB a) (DD b) F (D8 c)
TAddC' a b T c => TAddC' (DB a) (DC b) F (D7 c)
TAddC' a b T c => TAddC' (DB a) (DB b) F (D6 c)
TAddC' a b T c => TAddC' (DB a) (DA b) F (D5 c)
TAddC' a b T c => TAddC' (DB a) (D9 b) F (D4 c)
TAddC' a b T c => TAddC' (DB a) (D8 b) F (D3 c)
TAddC' a b T c => TAddC' (DB a) (D7 b) F (D2 c)
TAddC' a b T c => TAddC' (DB a) (D6 b) F (D1 c)
TAddC' a b T c => TAddC' (DB a) (D5 b) F (D0 c)
TAddC' a b F c => TAddC' (DB a) (D4 b) F (DF c)
TAddC' a b F c => TAddC' (DB a) (D3 b) F (DE c)
TAddC' a b F c => TAddC' (DB a) (D2 b) F (DD c)
TAddC' a b F c => TAddC' (DB a) (D1 b) F (DC c)
TAddC' a b F c => TAddC' (DB a) (D0 b) F (DB c)
TAddC' a b T c => TAddC' (DA a) (DF b) F (D9 c)
TAddC' a b T c => TAddC' (DA a) (DE b) F (D8 c)
TAddC' a b T c => TAddC' (DA a) (DD b) F (D7 c)
TAddC' a b T c => TAddC' (DA a) (DC b) F (D6 c)
TAddC' a b T c => TAddC' (DA a) (DB b) F (D5 c)
TAddC' a b T c => TAddC' (DA a) (DA b) F (D4 c)
TAddC' a b T c => TAddC' (DA a) (D9 b) F (D3 c)
TAddC' a b T c => TAddC' (DA a) (D8 b) F (D2 c)
TAddC' a b T c => TAddC' (DA a) (D7 b) F (D1 c)
TAddC' a b T c => TAddC' (DA a) (D6 b) F (D0 c)
TAddC' a b F c => TAddC' (DA a) (D5 b) F (DF c)
TAddC' a b F c => TAddC' (DA a) (D4 b) F (DE c)
TAddC' a b F c => TAddC' (DA a) (D3 b) F (DD c)
TAddC' a b F c => TAddC' (DA a) (D2 b) F (DC c)
TAddC' a b F c => TAddC' (DA a) (D1 b) F (DB c)
TAddC' a b F c => TAddC' (DA a) (D0 b) F (DA c)
TAddC' a b T c => TAddC' (D9 a) (DF b) F (D8 c)
TAddC' a b T c => TAddC' (D9 a) (DE b) F (D7 c)
TAddC' a b T c => TAddC' (D9 a) (DD b) F (D6 c)
TAddC' a b T c => TAddC' (D9 a) (DC b) F (D5 c)
TAddC' a b T c => TAddC' (D9 a) (DB b) F (D4 c)
TAddC' a b T c => TAddC' (D9 a) (DA b) F (D3 c)
TAddC' a b T c => TAddC' (D9 a) (D9 b) F (D2 c)
TAddC' a b T c => TAddC' (D9 a) (D8 b) F (D1 c)
TAddC' a b T c => TAddC' (D9 a) (D7 b) F (D0 c)
TAddC' a b F c => TAddC' (D9 a) (D6 b) F (DF c)
TAddC' a b F c => TAddC' (D9 a) (D5 b) F (DE c)
TAddC' a b F c => TAddC' (D9 a) (D4 b) F (DD c)
TAddC' a b F c => TAddC' (D9 a) (D3 b) F (DC c)
TAddC' a b F c => TAddC' (D9 a) (D2 b) F (DB c)
TAddC' a b F c => TAddC' (D9 a) (D1 b) F (DA c)
TAddC' a b F c => TAddC' (D9 a) (D0 b) F (D9 c)
TAddC' a b T c => TAddC' (D8 a) (DF b) F (D7 c)
TAddC' a b T c => TAddC' (D8 a) (DE b) F (D6 c)
TAddC' a b T c => TAddC' (D8 a) (DD b) F (D5 c)
TAddC' a b T c => TAddC' (D8 a) (DC b) F (D4 c)
TAddC' a b T c => TAddC' (D8 a) (DB b) F (D3 c)
TAddC' a b T c => TAddC' (D8 a) (DA b) F (D2 c)
TAddC' a b T c => TAddC' (D8 a) (D9 b) F (D1 c)
TAddC' a b T c => TAddC' (D8 a) (D8 b) F (D0 c)
TAddC' a b F c => TAddC' (D8 a) (D7 b) F (DF c)
TAddC' a b F c => TAddC' (D8 a) (D6 b) F (DE c)
TAddC' a b F c => TAddC' (D8 a) (D5 b) F (DD c)
TAddC' a b F c => TAddC' (D8 a) (D4 b) F (DC c)
TAddC' a b F c => TAddC' (D8 a) (D3 b) F (DB c)
TAddC' a b F c => TAddC' (D8 a) (D2 b) F (DA c)
TAddC' a b F c => TAddC' (D8 a) (D1 b) F (D9 c)
TAddC' a b F c => TAddC' (D8 a) (D0 b) F (D8 c)
TAddC' a b T c => TAddC' (D7 a) (DF b) F (D6 c)
TAddC' a b T c => TAddC' (D7 a) (DE b) F (D5 c)
TAddC' a b T c => TAddC' (D7 a) (DD b) F (D4 c)
TAddC' a b T c => TAddC' (D7 a) (DC b) F (D3 c)
TAddC' a b T c => TAddC' (D7 a) (DB b) F (D2 c)
TAddC' a b T c => TAddC' (D7 a) (DA b) F (D1 c)
TAddC' a b T c => TAddC' (D7 a) (D9 b) F (D0 c)
TAddC' a b F c => TAddC' (D7 a) (D8 b) F (DF c)
TAddC' a b F c => TAddC' (D7 a) (D7 b) F (DE c)
TAddC' a b F c => TAddC' (D7 a) (D6 b) F (DD c)
TAddC' a b F c => TAddC' (D7 a) (D5 b) F (DC c)
TAddC' a b F c => TAddC' (D7 a) (D4 b) F (DB c)
TAddC' a b F c => TAddC' (D7 a) (D3 b) F (DA c)
TAddC' a b F c => TAddC' (D7 a) (D2 b) F (D9 c)
TAddC' a b F c => TAddC' (D7 a) (D1 b) F (D8 c)
TAddC' a b F c => TAddC' (D7 a) (D0 b) F (D7 c)
TAddC' a b T c => TAddC' (D6 a) (DF b) F (D5 c)
TAddC' a b T c => TAddC' (D6 a) (DE b) F (D4 c)
TAddC' a b T c => TAddC' (D6 a) (DD b) F (D3 c)
TAddC' a b T c => TAddC' (D6 a) (DC b) F (D2 c)
TAddC' a b T c => TAddC' (D6 a) (DB b) F (D1 c)
TAddC' a b T c => TAddC' (D6 a) (DA b) F (D0 c)
TAddC' a b F c => TAddC' (D6 a) (D9 b) F (DF c)
TAddC' a b F c => TAddC' (D6 a) (D8 b) F (DE c)
TAddC' a b F c => TAddC' (D6 a) (D7 b) F (DD c)
TAddC' a b F c => TAddC' (D6 a) (D6 b) F (DC c)
TAddC' a b F c => TAddC' (D6 a) (D5 b) F (DB c)
TAddC' a b F c => TAddC' (D6 a) (D4 b) F (DA c)
TAddC' a b F c => TAddC' (D6 a) (D3 b) F (D9 c)
TAddC' a b F c => TAddC' (D6 a) (D2 b) F (D8 c)
TAddC' a b F c => TAddC' (D6 a) (D1 b) F (D7 c)
TAddC' a b F c => TAddC' (D6 a) (D0 b) F (D6 c)
TAddC' a b T c => TAddC' (D5 a) (DF b) F (D4 c)
TAddC' a b T c => TAddC' (D5 a) (DE b) F (D3 c)
TAddC' a b T c => TAddC' (D5 a) (DD b) F (D2 c)
TAddC' a b T c => TAddC' (D5 a) (DC b) F (D1 c)
TAddC' a b T c => TAddC' (D5 a) (DB b) F (D0 c)
TAddC' a b F c => TAddC' (D5 a) (DA b) F (DF c)
TAddC' a b F c => TAddC' (D5 a) (D9 b) F (DE c)
TAddC' a b F c => TAddC' (D5 a) (D8 b) F (DD c)
TAddC' a b F c => TAddC' (D5 a) (D7 b) F (DC c)
TAddC' a b F c => TAddC' (D5 a) (D6 b) F (DB c)
TAddC' a b F c => TAddC' (D5 a) (D5 b) F (DA c)
TAddC' a b F c => TAddC' (D5 a) (D4 b) F (D9 c)
TAddC' a b F c => TAddC' (D5 a) (D3 b) F (D8 c)
TAddC' a b F c => TAddC' (D5 a) (D2 b) F (D7 c)
TAddC' a b F c => TAddC' (D5 a) (D1 b) F (D6 c)
TAddC' a b F c => TAddC' (D5 a) (D0 b) F (D5 c)
TAddC' a b T c => TAddC' (D4 a) (DF b) F (D3 c)
TAddC' a b T c => TAddC' (D4 a) (DE b) F (D2 c)
TAddC' a b T c => TAddC' (D4 a) (DD b) F (D1 c)
TAddC' a b T c => TAddC' (D4 a) (DC b) F (D0 c)
TAddC' a b F c => TAddC' (D4 a) (DB b) F (DF c)
TAddC' a b F c => TAddC' (D4 a) (DA b) F (DE c)
TAddC' a b F c => TAddC' (D4 a) (D9 b) F (DD c)
TAddC' a b F c => TAddC' (D4 a) (D8 b) F (DC c)
TAddC' a b F c => TAddC' (D4 a) (D7 b) F (DB c)
TAddC' a b F c => TAddC' (D4 a) (D6 b) F (DA c)
TAddC' a b F c => TAddC' (D4 a) (D5 b) F (D9 c)
TAddC' a b F c => TAddC' (D4 a) (D4 b) F (D8 c)
TAddC' a b F c => TAddC' (D4 a) (D3 b) F (D7 c)
TAddC' a b F c => TAddC' (D4 a) (D2 b) F (D6 c)
TAddC' a b F c => TAddC' (D4 a) (D1 b) F (D5 c)
TAddC' a b F c => TAddC' (D4 a) (D0 b) F (D4 c)
TAddC' a b T c => TAddC' (D3 a) (DF b) F (D2 c)
TAddC' a b T c => TAddC' (D3 a) (DE b) F (D1 c)
TAddC' a b T c => TAddC' (D3 a) (DD b) F (D0 c)
TAddC' a b F c => TAddC' (D3 a) (DC b) F (DF c)
TAddC' a b F c => TAddC' (D3 a) (DB b) F (DE c)
TAddC' a b F c => TAddC' (D3 a) (DA b) F (DD c)
TAddC' a b F c => TAddC' (D3 a) (D9 b) F (DC c)
TAddC' a b F c => TAddC' (D3 a) (D8 b) F (DB c)
TAddC' a b F c => TAddC' (D3 a) (D7 b) F (DA c)
TAddC' a b F c => TAddC' (D3 a) (D6 b) F (D9 c)
TAddC' a b F c => TAddC' (D3 a) (D5 b) F (D8 c)
TAddC' a b F c => TAddC' (D3 a) (D4 b) F (D7 c)
TAddC' a b F c => TAddC' (D3 a) (D3 b) F (D6 c)
TAddC' a b F c => TAddC' (D3 a) (D2 b) F (D5 c)
TAddC' a b F c => TAddC' (D3 a) (D1 b) F (D4 c)
TAddC' a b F c => TAddC' (D3 a) (D0 b) F (D3 c)
TAddC' a b T c => TAddC' (D2 a) (DF b) F (D1 c)
TAddC' a b T c => TAddC' (D2 a) (DE b) F (D0 c)
TAddC' a b F c => TAddC' (D2 a) (DD b) F (DF c)
TAddC' a b F c => TAddC' (D2 a) (DC b) F (DE c)
TAddC' a b F c => TAddC' (D2 a) (DB b) F (DD c)
TAddC' a b F c => TAddC' (D2 a) (DA b) F (DC c)
TAddC' a b F c => TAddC' (D2 a) (D9 b) F (DB c)
TAddC' a b F c => TAddC' (D2 a) (D8 b) F (DA c)
TAddC' a b F c => TAddC' (D2 a) (D7 b) F (D9 c)
TAddC' a b F c => TAddC' (D2 a) (D6 b) F (D8 c)
TAddC' a b F c => TAddC' (D2 a) (D5 b) F (D7 c)
TAddC' a b F c => TAddC' (D2 a) (D4 b) F (D6 c)
TAddC' a b F c => TAddC' (D2 a) (D3 b) F (D5 c)
TAddC' a b F c => TAddC' (D2 a) (D2 b) F (D4 c)
TAddC' a b F c => TAddC' (D2 a) (D1 b) F (D3 c)
TAddC' a b F c => TAddC' (D2 a) (D0 b) F (D2 c)
TAddC' a b T c => TAddC' (D1 a) (DF b) F (D0 c)
TAddC' a b F c => TAddC' (D1 a) (DE b) F (DF c)
TAddC' a b F c => TAddC' (D1 a) (DD b) F (DE c)
TAddC' a b F c => TAddC' (D1 a) (DC b) F (DD c)
TAddC' a b F c => TAddC' (D1 a) (DB b) F (DC c)
TAddC' a b F c => TAddC' (D1 a) (DA b) F (DB c)
TAddC' a b F c => TAddC' (D1 a) (D9 b) F (DA c)
TAddC' a b F c => TAddC' (D1 a) (D8 b) F (D9 c)
TAddC' a b F c => TAddC' (D1 a) (D7 b) F (D8 c)
TAddC' a b F c => TAddC' (D1 a) (D6 b) F (D7 c)
TAddC' a b F c => TAddC' (D1 a) (D5 b) F (D6 c)
TAddC' a b F c => TAddC' (D1 a) (D4 b) F (D5 c)
TAddC' a b F c => TAddC' (D1 a) (D3 b) F (D4 c)
TAddC' a b F c => TAddC' (D1 a) (D2 b) F (D3 c)
TAddC' a b F c => TAddC' (D1 a) (D1 b) F (D2 c)
TAddC' a b F c => TAddC' (D1 a) (D0 b) F (D1 c)
TAddC' a b F c => TAddC' (D0 a) (DF b) F (DF c)
TAddC' a b F c => TAddC' (D0 a) (DE b) F (DE c)
TAddC' a b F c => TAddC' (D0 a) (DD b) F (DD c)
TAddC' a b F c => TAddC' (D0 a) (DC b) F (DC c)
TAddC' a b F c => TAddC' (D0 a) (DB b) F (DB c)
TAddC' a b F c => TAddC' (D0 a) (DA b) F (DA c)
TAddC' a b F c => TAddC' (D0 a) (D9 b) F (D9 c)
TAddC' a b F c => TAddC' (D0 a) (D8 b) F (D8 c)
TAddC' a b F c => TAddC' (D0 a) (D7 b) F (D7 c)
TAddC' a b F c => TAddC' (D0 a) (D6 b) F (D6 c)
TAddC' a b F c => TAddC' (D0 a) (D5 b) F (D5 c)
TAddC' a b F c => TAddC' (D0 a) (D4 b) F (D4 c)
TAddC' a b F c => TAddC' (D0 a) (D3 b) F (D3 c)
TAddC' a b F c => TAddC' (D0 a) (D2 b) F (D2 c)
TAddC' a b F c => TAddC' (D0 a) (D1 b) F (D1 c)
TAddC' a b F c => TAddC' (D0 a) (D0 b) F (D0 c)

data T Source

Instances

Show T	Let them be shown
TBool T
TBinary T
THex T
TNot F T
TNot T F
TCBool Closure T
Trichotomy T Negative
TCBinary Closure T
TSucc T F
TSucc T F
TEven F T
TEven T F
Trichotomy T Negative
THex2Binary' T T
TImplies F F T
TImplies F T T
TImplies T F F
TImplies T T T
TXOr' F T T
TXOr' T F T
TXOr' T T F
TOr F T T
TOr T F T
TOr T T T
TAnd F T F
TAnd T F F
TAnd T T T
TEq F F T
TEq F T F
TEq T F F
TEq T T T
TEq Positive Positive T
TEq SignZero SignZero T
TEq Negative Negative T
TEq TNothing TNothing T
TCountBits' T T T
TShift' F T F
TShift' T F T
TShift' T T T
TNeg a b => TMul a T b
TNF' T T F
LSB T T T
TNF' T T F
LSN T HF T
TNeg a b => TMul a T b
TIf T x y x
TAddC' F T F T
TAddC' F T T F
TAddC' T F F T
TAddC' T F T F
TAddC' T T T T
TAddC' F T F T
TAddC' F T T F
TAddC' T F F T
TAddC' T F T F
TAddC' T T T T
TAddC' F F T (I F)
TAddC' T T F (O T)
TAddC' F F T (D1 F)
TAddC' T T F (DE T)
SHR1 H1 T (DE T)
SHR1 H0 T (DE T)
TImplies F (I b) T
TImplies F (O b) T
TOr T (I b) T
TOr T (O b) T
TLt TNothing (TJust b) T
TSucc a b => TAddC' F (I a) T (O b)
TAddC' F (O a) T (I a)
TAddC' T (I a) F (O a)
TAddC' T (I a) T (I a)
TSucc b a => TAddC' T (O a) F (I b)
TAddC' T (O a) T (O a)
TSucc a b => TAddC' F (DF a) T (D0 b)
TAddC' F (DE a) T (DF a)
TAddC' F (DD a) T (DE a)
TAddC' F (DC a) T (DD a)
TAddC' F (DB a) T (DC a)
TAddC' F (DA a) T (DB a)
TAddC' F (D9 a) T (DA a)
TAddC' F (D8 a) T (D9 a)
TAddC' F (D7 a) T (D8 a)
TAddC' F (D6 a) T (D7 a)
TAddC' F (D5 a) T (D6 a)
TAddC' F (D4 a) T (D5 a)
TAddC' F (D3 a) T (D4 a)
TAddC' F (D2 a) T (D3 a)
TAddC' F (D1 a) T (D2 a)
TAddC' F (D0 a) T (D1 a)
TAddC' T (DF a) T (DF a)
TAddC' T (DF a) F (DE a)
TAddC' T (DE a) T (DE a)
TAddC' T (DE a) F (DD a)
TAddC' T (DD a) T (DD a)
TAddC' T (DD a) F (DC a)
TAddC' T (DC a) T (DC a)
TAddC' T (DC a) F (DB a)
TAddC' T (DB a) T (DB a)
TAddC' T (DB a) F (DA a)
TAddC' T (DA a) T (DA a)
TAddC' T (DA a) F (D9 a)
TAddC' T (D9 a) T (D9 a)
TAddC' T (D9 a) F (D8 a)
TAddC' T (D8 a) T (D8 a)
TAddC' T (D8 a) F (D7 a)
TAddC' T (D7 a) T (D7 a)
TAddC' T (D7 a) F (D6 a)
TAddC' T (D6 a) T (D6 a)
TAddC' T (D6 a) F (D5 a)
TAddC' T (D5 a) T (D5 a)
TAddC' T (D5 a) F (D4 a)
TAddC' T (D4 a) T (D4 a)
TAddC' T (D4 a) F (D3 a)
TAddC' T (D3 a) T (D3 a)
TAddC' T (D3 a) F (D2 a)
TAddC' T (D2 a) T (D2 a)
TAddC' T (D2 a) F (D1 a)
TAddC' T (D1 a) T (D1 a)
TAddC' T (D1 a) F (D0 a)
TSucc b a => TAddC' T (D0 a) F (DF b)
TAddC' T (D0 a) T (D0 a)
TImplies T (I b) (I b)
TImplies T (O b) (O b)
TNot b c => TXOr' T (I b) (O c)
TNot b c => TXOr' T (O b) (I c)
TAnd T (I b) (I b)
TAnd T (O b) (O b)
SHR1 H1 (DF T) (DF T)
SHR1 H1 (DE T) (DD T)
SHR1 H1 (DD T) (DB T)
SHR1 H1 (DC T) (D9 T)
SHR1 H1 (DB T) (D7 T)
SHR1 H1 (DA T) (D5 T)
SHR1 H1 (D9 T) (D3 T)
SHR1 H1 (D8 T) (D1 T)
SHR1 H1 (D7 T) (DF (DE T))
SHR1 H1 (D6 T) (DD (DE T))
SHR1 H1 (D5 T) (DB (DE T))
SHR1 H1 (D4 T) (D9 (DE T))
SHR1 H1 (D3 T) (D7 (DE T))
SHR1 H1 (D2 T) (D5 (DE T))
SHR1 H1 (D1 T) (D3 (DE T))
SHR1 H1 (D0 T) (D1 (DE T))
SHR1 H0 (DF T) (DE T)
SHR1 H0 (DE T) (DC T)
SHR1 H0 (DD T) (DA T)
SHR1 H0 (DC T) (D8 T)
SHR1 H0 (DB T) (D6 T)
SHR1 H0 (DA T) (D4 T)
SHR1 H0 (D9 T) (D2 T)
SHR1 H0 (D8 T) (D0 T)
SHR1 H0 (D7 T) (DE (DE T))
SHR1 H0 (D6 T) (DC (DE T))
SHR1 H0 (D5 T) (DA (DE T))
SHR1 H0 (D4 T) (D8 (DE T))
SHR1 H0 (D3 T) (D6 (DE T))
SHR1 H0 (D2 T) (D4 (DE T))
SHR1 H0 (D1 T) (D2 (DE T))
SHR1 H0 (D0 T) (D0 (DE T))
Trichotomy (O T) Negative
TSucc (O T) T
TSucc (DE T) T
TEven (DE a) T
TEven (DC a) T
TEven (DA a) T
TEven (D8 a) T
TEven (D6 a) T
TEven (D4 a) T
TEven (D2 a) T
TEven (D0 a) T
Trichotomy (DE T) Negative
Trichotomy (DD T) Negative
Trichotomy (DC T) Negative
Trichotomy (DB T) Negative
Trichotomy (DA T) Negative
Trichotomy (D9 T) Negative
Trichotomy (D8 T) Negative
Trichotomy (D7 T) Negative
Trichotomy (D6 T) Negative
Trichotomy (D5 T) Negative
Trichotomy (D4 T) Negative
Trichotomy (D3 T) Negative
Trichotomy (D2 T) Negative
Trichotomy (D1 T) Negative
Trichotomy (D0 T) Negative
TImplies (I a) F T
TImplies (O a) F T
TOr (I a) T T
TOr (O a) T T
TEq (I m) T F
TEq (O m) T F
TCountBits' a m F => TCountBits' (I a) m T
(TCountBits' a n F, TSucc m n) => TCountBits' (O a) n T
TShift' (I a) T a
TShift' (O a) T a
TNF' (I T) T F
LSB (I a) T a => X (I a) T a
LSB (I F) T F
LSB (O T) F T
TNF' (DF T) T F
LSN (DE T) HE T
LSN (DD T) HD T
LSN (DC T) HC T
LSN (DB T) HB T
LSN (DA T) HA T
LSN (D9 T) H9 T
LSN (D8 T) H8 T
LSN (D7 T) H7 T
LSN (D6 T) H6 T
LSN (D5 T) H5 T
LSN (D4 T) H4 T
LSN (D3 T) H3 T
LSN (D2 T) H2 T
LSN (D1 T) H1 T
LSN (D0 T) H0 T
TSucc a b => TAddC' (I a) F T (O b)
TAddC' (I a) T F (O a)
TAddC' (I a) T T (I a)
TSucc b a => TAddC' (O a) T F (I b)
TAddC' (O a) F T (I a)
TAddC' (O a) T T (O a)
TSucc a b => TAddC' (DF a) F T (D0 b)
TAddC' (DF a) T T (DF a)
TAddC' (DF a) T F (DE a)
TAddC' (DE a) T T (DE a)
TAddC' (DE a) F T (DF a)
TAddC' (DE a) T F (DD a)
TAddC' (DD a) T T (DD a)
TAddC' (DD a) F T (DE a)
TAddC' (DD a) T F (DC a)
TAddC' (DC a) T T (DC a)
TAddC' (DC a) F T (DD a)
TAddC' (DC a) T F (DB a)
TAddC' (DB a) T T (DB a)
TAddC' (DB a) F T (DC a)
TAddC' (DB a) T F (DA a)
TAddC' (DA a) T T (DA a)
TAddC' (DA a) F T (DB a)
TAddC' (DA a) T F (D9 a)
TAddC' (D9 a) T T (D9 a)
TAddC' (D9 a) F T (DA a)
TAddC' (D9 a) T F (D8 a)
TAddC' (D8 a) T T (D8 a)
TAddC' (D8 a) F T (D9 a)
TAddC' (D8 a) T F (D7 a)
TAddC' (D7 a) T T (D7 a)
TAddC' (D7 a) F T (D8 a)
TAddC' (D7 a) T F (D6 a)
TAddC' (D6 a) T T (D6 a)
TAddC' (D6 a) F T (D7 a)
TAddC' (D6 a) T F (D5 a)
TAddC' (D5 a) T T (D5 a)
TAddC' (D5 a) F T (D6 a)
TAddC' (D5 a) T F (D4 a)
TAddC' (D4 a) T T (D4 a)
TAddC' (D4 a) F T (D5 a)
TAddC' (D4 a) T F (D3 a)
TAddC' (D3 a) T T (D3 a)
TAddC' (D3 a) F T (D4 a)
TAddC' (D3 a) T F (D2 a)
TAddC' (D2 a) T T (D2 a)
TAddC' (D2 a) F T (D3 a)
TAddC' (D2 a) T F (D1 a)
TAddC' (D1 a) T T (D1 a)
TAddC' (D1 a) F T (D2 a)
TAddC' (D1 a) T F (D0 a)
TSucc b a => TAddC' (D0 a) T F (DF b)
TAddC' (D0 a) T T (D0 a)
TAddC' (D0 a) F T (D1 a)
TImplies (I a) T (I a)
TImplies (O a) T (O a)
TNot b c => TXOr' (I b) T (O c)
TNot b c => TXOr' (O b) T (I c)
TAnd (I a) T (I a)
TAnd (O a) T (O a)
LSB (I (I n)) T (I n)
LSB (I (O n)) T (O n)
TSucc (DD T) (DE T)
TSucc (DC T) (DD T)
TSucc (DB T) (DC T)
TSucc (DA T) (DB T)
TSucc (D9 T) (DA T)
TSucc (D8 T) (D9 T)
TSucc (D7 T) (D8 T)
TSucc (D6 T) (D7 T)
TSucc (D5 T) (D6 T)
TSucc (D4 T) (D5 T)
TSucc (D3 T) (D4 T)
TSucc (D2 T) (D3 T)
TSucc (D1 T) (D2 T)
TSucc (D0 T) (D1 T)
TNF' (I F) (I F) T
TNF' (O a) c b => TNF' (I (O a)) (I c) T
TNF' (O T) (O T) T
TNF' (I a) c b => TNF' (O (I a)) (O c) T
TNF' (DF F) (DF F) T
TNF' (DE F) (DE F) T
TNF' (DE T) (DE T) T
TNF' (DD F) (DD F) T
TNF' (DD T) (DD T) T
TNF' (DC F) (DC F) T
TNF' (DC T) (DC T) T
TNF' (DB F) (DB F) T
TNF' (DB T) (DB T) T
TNF' (DA F) (DA F) T
TNF' (DA T) (DA T) T
TNF' (D9 F) (D9 F) T
TNF' (D9 T) (D9 T) T
TNF' (D8 F) (D8 F) T
TNF' (D8 T) (D8 T) T
TNF' (D7 F) (D7 F) T
TNF' (D7 T) (D7 T) T
TNF' (D6 F) (D6 F) T
TNF' (D6 T) (D6 T) T
TNF' (D5 F) (D5 F) T
TNF' (D5 T) (D5 T) T
TNF' (D4 F) (D4 F) T
TNF' (D4 T) (D4 T) T
TNF' (D3 F) (D3 F) T
TNF' (D3 T) (D3 T) T
TNF' (D2 F) (D2 F) T
TNF' (D2 T) (D2 T) T
TNF' (D1 F) (D1 F) T
TNF' (D1 T) (D1 T) T
TNF' (D0 T) (D0 T) T
TAddC' a b T c => TAddC' (I a) (I b) T (I c)
TAddC' a b T c => TAddC' (I a) (O b) T (O c)
TAddC' a b T c => TAddC' (O a) (I b) T (O c)
TAddC' a b F c => TAddC' (O a) (O b) T (I c)
TAddC' a b T c => TAddC' (DF a) (DF b) T (DF c)
TAddC' a b T c => TAddC' (DF a) (DE b) T (DE c)
TAddC' a b T c => TAddC' (DF a) (DD b) T (DD c)
TAddC' a b T c => TAddC' (DF a) (DC b) T (DC c)
TAddC' a b T c => TAddC' (DF a) (DB b) T (DB c)
TAddC' a b T c => TAddC' (DF a) (DA b) T (DA c)
TAddC' a b T c => TAddC' (DF a) (D9 b) T (D9 c)
TAddC' a b T c => TAddC' (DF a) (D8 b) T (D8 c)
TAddC' a b T c => TAddC' (DF a) (D7 b) T (D7 c)
TAddC' a b T c => TAddC' (DF a) (D6 b) T (D6 c)
TAddC' a b T c => TAddC' (DF a) (D5 b) T (D5 c)
TAddC' a b T c => TAddC' (DF a) (D4 b) T (D4 c)
TAddC' a b T c => TAddC' (DF a) (D3 b) T (D3 c)
TAddC' a b T c => TAddC' (DF a) (D2 b) T (D2 c)
TAddC' a b T c => TAddC' (DF a) (D1 b) T (D1 c)
TAddC' a b T c => TAddC' (DF a) (D0 b) T (D0 c)
TAddC' a b T c => TAddC' (DE a) (DF b) T (DE c)
TAddC' a b T c => TAddC' (DE a) (DE b) T (DD c)
TAddC' a b T c => TAddC' (DE a) (DD b) T (DC c)
TAddC' a b T c => TAddC' (DE a) (DC b) T (DB c)
TAddC' a b T c => TAddC' (DE a) (DB b) T (DA c)
TAddC' a b T c => TAddC' (DE a) (DA b) T (D9 c)
TAddC' a b T c => TAddC' (DE a) (D9 b) T (D8 c)
TAddC' a b T c => TAddC' (DE a) (D8 b) T (D7 c)
TAddC' a b T c => TAddC' (DE a) (D7 b) T (D6 c)
TAddC' a b T c => TAddC' (DE a) (D6 b) T (D5 c)
TAddC' a b T c => TAddC' (DE a) (D5 b) T (D4 c)
TAddC' a b T c => TAddC' (DE a) (D4 b) T (D3 c)
TAddC' a b T c => TAddC' (DE a) (D3 b) T (D2 c)
TAddC' a b T c => TAddC' (DE a) (D2 b) T (D1 c)
TAddC' a b T c => TAddC' (DE a) (D1 b) T (D0 c)
TAddC' a b F c => TAddC' (DE a) (D0 b) T (DF c)
TAddC' a b T c => TAddC' (DD a) (DF b) T (DD c)
TAddC' a b T c => TAddC' (DD a) (DE b) T (DC c)
TAddC' a b T c => TAddC' (DD a) (DD b) T (DB c)
TAddC' a b T c => TAddC' (DD a) (DC b) T (DA c)
TAddC' a b T c => TAddC' (DD a) (DB b) T (D9 c)
TAddC' a b T c => TAddC' (DD a) (DA b) T (D8 c)
TAddC' a b T c => TAddC' (DD a) (D9 b) T (D7 c)
TAddC' a b T c => TAddC' (DD a) (D8 b) T (D6 c)
TAddC' a b T c => TAddC' (DD a) (D7 b) T (D5 c)
TAddC' a b T c => TAddC' (DD a) (D6 b) T (D4 c)
TAddC' a b T c => TAddC' (DD a) (D5 b) T (D3 c)
TAddC' a b T c => TAddC' (DD a) (D4 b) T (D2 c)
TAddC' a b T c => TAddC' (DD a) (D3 b) T (D1 c)
TAddC' a b T c => TAddC' (DD a) (D2 b) T (D0 c)
TAddC' a b F c => TAddC' (DD a) (D1 b) T (DF c)
TAddC' a b F c => TAddC' (DD a) (D0 b) T (DE c)
TAddC' a b T c => TAddC' (DC a) (DF b) T (DC c)
TAddC' a b T c => TAddC' (DC a) (DE b) T (DB c)
TAddC' a b T c => TAddC' (DC a) (DD b) T (DA c)
TAddC' a b T c => TAddC' (DC a) (DC b) T (D9 c)
TAddC' a b T c => TAddC' (DC a) (DB b) T (D8 c)
TAddC' a b T c => TAddC' (DC a) (DA b) T (D7 c)
TAddC' a b T c => TAddC' (DC a) (D9 b) T (D6 c)
TAddC' a b T c => TAddC' (DC a) (D8 b) T (D5 c)
TAddC' a b T c => TAddC' (DC a) (D7 b) T (D4 c)
TAddC' a b T c => TAddC' (DC a) (D6 b) T (D3 c)
TAddC' a b T c => TAddC' (DC a) (D5 b) T (D2 c)
TAddC' a b T c => TAddC' (DC a) (D4 b) T (D1 c)
TAddC' a b T c => TAddC' (DC a) (D3 b) T (D0 c)
TAddC' a b F c => TAddC' (DC a) (D2 b) T (DF c)
TAddC' a b F c => TAddC' (DC a) (D1 b) T (DE c)
TAddC' a b F c => TAddC' (DC a) (D0 b) T (DD c)
TAddC' a b T c => TAddC' (DB a) (DF b) T (DB c)
TAddC' a b T c => TAddC' (DB a) (DE b) T (DA c)
TAddC' a b T c => TAddC' (DB a) (DD b) T (D9 c)
TAddC' a b T c => TAddC' (DB a) (DC b) T (D8 c)
TAddC' a b T c => TAddC' (DB a) (DB b) T (D7 c)
TAddC' a b T c => TAddC' (DB a) (DA b) T (D6 c)
TAddC' a b T c => TAddC' (DB a) (D9 b) T (D5 c)
TAddC' a b T c => TAddC' (DB a) (D8 b) T (D4 c)
TAddC' a b T c => TAddC' (DB a) (D7 b) T (D3 c)
TAddC' a b T c => TAddC' (DB a) (D6 b) T (D2 c)
TAddC' a b T c => TAddC' (DB a) (D5 b) T (D1 c)
TAddC' a b T c => TAddC' (DB a) (D4 b) T (D0 c)
TAddC' a b F c => TAddC' (DB a) (D3 b) T (DF c)
TAddC' a b F c => TAddC' (DB a) (D2 b) T (DE c)
TAddC' a b F c => TAddC' (DB a) (D1 b) T (DD c)
TAddC' a b F c => TAddC' (DB a) (D0 b) T (DC c)
TAddC' a b T c => TAddC' (DA a) (DF b) T (DA c)
TAddC' a b T c => TAddC' (DA a) (DE b) T (D9 c)
TAddC' a b T c => TAddC' (DA a) (DD b) T (D8 c)
TAddC' a b T c => TAddC' (DA a) (DC b) T (D7 c)
TAddC' a b T c => TAddC' (DA a) (DB b) T (D6 c)
TAddC' a b T c => TAddC' (DA a) (DA b) T (D5 c)
TAddC' a b T c => TAddC' (DA a) (D9 b) T (D4 c)
TAddC' a b T c => TAddC' (DA a) (D8 b) T (D3 c)
TAddC' a b T c => TAddC' (DA a) (D7 b) T (D2 c)
TAddC' a b T c => TAddC' (DA a) (D6 b) T (D1 c)
TAddC' a b T c => TAddC' (DA a) (D5 b) T (D0 c)
TAddC' a b F c => TAddC' (DA a) (D4 b) T (DF c)
TAddC' a b F c => TAddC' (DA a) (D3 b) T (DE c)
TAddC' a b F c => TAddC' (DA a) (D2 b) T (DD c)
TAddC' a b F c => TAddC' (DA a) (D1 b) T (DC c)
TAddC' a b F c => TAddC' (DA a) (D0 b) T (DB c)
TAddC' a b T c => TAddC' (D9 a) (DF b) T (D9 c)
TAddC' a b T c => TAddC' (D9 a) (DE b) T (D8 c)
TAddC' a b T c => TAddC' (D9 a) (DD b) T (D7 c)
TAddC' a b T c => TAddC' (D9 a) (DC b) T (D6 c)
TAddC' a b T c => TAddC' (D9 a) (DB b) T (D5 c)
TAddC' a b T c => TAddC' (D9 a) (DA b) T (D4 c)
TAddC' a b T c => TAddC' (D9 a) (D9 b) T (D3 c)
TAddC' a b T c => TAddC' (D9 a) (D8 b) T (D2 c)
TAddC' a b T c => TAddC' (D9 a) (D7 b) T (D1 c)
TAddC' a b T c => TAddC' (D9 a) (D6 b) T (D0 c)
TAddC' a b F c => TAddC' (D9 a) (D5 b) T (DF c)
TAddC' a b F c => TAddC' (D9 a) (D4 b) T (DE c)
TAddC' a b F c => TAddC' (D9 a) (D3 b) T (DD c)
TAddC' a b F c => TAddC' (D9 a) (D2 b) T (DC c)
TAddC' a b F c => TAddC' (D9 a) (D1 b) T (DB c)
TAddC' a b F c => TAddC' (D9 a) (D0 b) T (DA c)
TAddC' a b T c => TAddC' (D8 a) (DF b) T (D8 c)
TAddC' a b T c => TAddC' (D8 a) (DE b) T (D7 c)
TAddC' a b T c => TAddC' (D8 a) (DD b) T (D6 c)
TAddC' a b T c => TAddC' (D8 a) (DC b) T (D5 c)
TAddC' a b T c => TAddC' (D8 a) (DB b) T (D4 c)
TAddC' a b T c => TAddC' (D8 a) (DA b) T (D3 c)
TAddC' a b T c => TAddC' (D8 a) (D9 b) T (D2 c)
TAddC' a b T c => TAddC' (D8 a) (D8 b) T (D1 c)
TAddC' a b T c => TAddC' (D8 a) (D7 b) T (D0 c)
TAddC' a b F c => TAddC' (D8 a) (D6 b) T (DF c)
TAddC' a b F c => TAddC' (D8 a) (D5 b) T (DE c)
TAddC' a b F c => TAddC' (D8 a) (D4 b) T (DD c)
TAddC' a b F c => TAddC' (D8 a) (D3 b) T (DC c)
TAddC' a b F c => TAddC' (D8 a) (D2 b) T (DB c)
TAddC' a b F c => TAddC' (D8 a) (D1 b) T (DA c)
TAddC' a b F c => TAddC' (D8 a) (D0 b) T (D9 c)
TAddC' a b T c => TAddC' (D7 a) (DF b) T (D7 c)
TAddC' a b T c => TAddC' (D7 a) (DE b) T (D6 c)
TAddC' a b T c => TAddC' (D7 a) (DD b) T (D5 c)
TAddC' a b T c => TAddC' (D7 a) (DC b) T (D4 c)
TAddC' a b T c => TAddC' (D7 a) (DB b) T (D3 c)
TAddC' a b T c => TAddC' (D7 a) (DA b) T (D2 c)
TAddC' a b T c => TAddC' (D7 a) (D9 b) T (D1 c)
TAddC' a b T c => TAddC' (D7 a) (D8 b) T (D0 c)
TAddC' a b F c => TAddC' (D7 a) (D7 b) T (DF c)
TAddC' a b F c => TAddC' (D7 a) (D6 b) T (DE c)
TAddC' a b F c => TAddC' (D7 a) (D5 b) T (DD c)
TAddC' a b F c => TAddC' (D7 a) (D4 b) T (DC c)
TAddC' a b F c => TAddC' (D7 a) (D3 b) T (DB c)
TAddC' a b F c => TAddC' (D7 a) (D2 b) T (DA c)
TAddC' a b F c => TAddC' (D7 a) (D1 b) T (D9 c)
TAddC' a b F c => TAddC' (D7 a) (D0 b) T (D8 c)
TAddC' a b T c => TAddC' (D6 a) (DF b) T (D6 c)
TAddC' a b T c => TAddC' (D6 a) (DE b) T (D5 c)
TAddC' a b T c => TAddC' (D6 a) (DD b) T (D4 c)
TAddC' a b T c => TAddC' (D6 a) (DC b) T (D3 c)
TAddC' a b T c => TAddC' (D6 a) (DB b) T (D2 c)
TAddC' a b T c => TAddC' (D6 a) (DA b) T (D1 c)
TAddC' a b T c => TAddC' (D6 a) (D9 b) T (D0 c)
TAddC' a b F c => TAddC' (D6 a) (D8 b) T (DF c)
TAddC' a b F c => TAddC' (D6 a) (D7 b) T (DE c)
TAddC' a b F c => TAddC' (D6 a) (D6 b) T (DD c)
TAddC' a b F c => TAddC' (D6 a) (D5 b) T (DC c)
TAddC' a b F c => TAddC' (D6 a) (D4 b) T (DB c)
TAddC' a b F c => TAddC' (D6 a) (D3 b) T (DA c)
TAddC' a b F c => TAddC' (D6 a) (D2 b) T (D9 c)
TAddC' a b F c => TAddC' (D6 a) (D1 b) T (D8 c)
TAddC' a b F c => TAddC' (D6 a) (D0 b) T (D7 c)
TAddC' a b T c => TAddC' (D5 a) (DF b) T (D5 c)
TAddC' a b T c => TAddC' (D5 a) (DE b) T (D4 c)
TAddC' a b T c => TAddC' (D5 a) (DD b) T (D3 c)
TAddC' a b T c => TAddC' (D5 a) (DC b) T (D2 c)
TAddC' a b T c => TAddC' (D5 a) (DB b) T (D1 c)
TAddC' a b T c => TAddC' (D5 a) (DA b) T (D0 c)
TAddC' a b F c => TAddC' (D5 a) (D9 b) T (DF c)
TAddC' a b F c => TAddC' (D5 a) (D8 b) T (DE c)
TAddC' a b F c => TAddC' (D5 a) (D7 b) T (DD c)
TAddC' a b F c => TAddC' (D5 a) (D6 b) T (DC c)
TAddC' a b F c => TAddC' (D5 a) (D5 b) T (DB c)
TAddC' a b F c => TAddC' (D5 a) (D4 b) T (DA c)
TAddC' a b F c => TAddC' (D5 a) (D3 b) T (D9 c)
TAddC' a b F c => TAddC' (D5 a) (D2 b) T (D8 c)
TAddC' a b F c => TAddC' (D5 a) (D1 b) T (D7 c)
TAddC' a b F c => TAddC' (D5 a) (D0 b) T (D6 c)
TAddC' a b T c => TAddC' (D4 a) (DF b) T (D4 c)
TAddC' a b T c => TAddC' (D4 a) (DE b) T (D3 c)
TAddC' a b T c => TAddC' (D4 a) (DD b) T (D2 c)
TAddC' a b T c => TAddC' (D4 a) (DC b) T (D1 c)
TAddC' a b T c => TAddC' (D4 a) (DB b) T (D0 c)
TAddC' a b F c => TAddC' (D4 a) (DA b) T (DF c)
TAddC' a b F c => TAddC' (D4 a) (D9 b) T (DE c)
TAddC' a b F c => TAddC' (D4 a) (D8 b) T (DD c)
TAddC' a b F c => TAddC' (D4 a) (D7 b) T (DC c)
TAddC' a b F c => TAddC' (D4 a) (D6 b) T (DB c)
TAddC' a b F c => TAddC' (D4 a) (D5 b) T (DA c)
TAddC' a b F c => TAddC' (D4 a) (D4 b) T (D9 c)
TAddC' a b F c => TAddC' (D4 a) (D3 b) T (D8 c)
TAddC' a b F c => TAddC' (D4 a) (D2 b) T (D7 c)
TAddC' a b F c => TAddC' (D4 a) (D1 b) T (D6 c)
TAddC' a b F c => TAddC' (D4 a) (D0 b) T (D5 c)
TAddC' a b T c => TAddC' (D3 a) (DF b) T (D3 c)
TAddC' a b T c => TAddC' (D3 a) (DE b) T (D2 c)
TAddC' a b T c => TAddC' (D3 a) (DD b) T (D1 c)
TAddC' a b T c => TAddC' (D3 a) (DC b) T (D0 c)
TAddC' a b F c => TAddC' (D3 a) (DB b) T (DF c)
TAddC' a b F c => TAddC' (D3 a) (DA b) T (DE c)
TAddC' a b F c => TAddC' (D3 a) (D9 b) T (DD c)
TAddC' a b F c => TAddC' (D3 a) (D8 b) T (DC c)
TAddC' a b F c => TAddC' (D3 a) (D7 b) T (DB c)
TAddC' a b F c => TAddC' (D3 a) (D6 b) T (DA c)
TAddC' a b F c => TAddC' (D3 a) (D5 b) T (D9 c)
TAddC' a b F c => TAddC' (D3 a) (D4 b) T (D8 c)
TAddC' a b F c => TAddC' (D3 a) (D3 b) T (D7 c)
TAddC' a b F c => TAddC' (D3 a) (D2 b) T (D6 c)
TAddC' a b F c => TAddC' (D3 a) (D1 b) T (D5 c)
TAddC' a b F c => TAddC' (D3 a) (D0 b) T (D4 c)
TAddC' a b T c => TAddC' (D2 a) (DF b) T (D2 c)
TAddC' a b T c => TAddC' (D2 a) (DE b) T (D1 c)
TAddC' a b T c => TAddC' (D2 a) (DD b) T (D0 c)
TAddC' a b F c => TAddC' (D2 a) (DC b) T (DF c)
TAddC' a b F c => TAddC' (D2 a) (DB b) T (DE c)
TAddC' a b F c => TAddC' (D2 a) (DA b) T (DD c)
TAddC' a b F c => TAddC' (D2 a) (D9 b) T (DC c)
TAddC' a b F c => TAddC' (D2 a) (D8 b) T (DB c)
TAddC' a b F c => TAddC' (D2 a) (D7 b) T (DA c)
TAddC' a b F c => TAddC' (D2 a) (D6 b) T (D9 c)
TAddC' a b F c => TAddC' (D2 a) (D5 b) T (D8 c)
TAddC' a b F c => TAddC' (D2 a) (D4 b) T (D7 c)
TAddC' a b F c => TAddC' (D2 a) (D3 b) T (D6 c)
TAddC' a b F c => TAddC' (D2 a) (D2 b) T (D5 c)
TAddC' a b F c => TAddC' (D2 a) (D1 b) T (D4 c)
TAddC' a b F c => TAddC' (D2 a) (D0 b) T (D3 c)
TAddC' a b T c => TAddC' (D1 a) (DF b) T (D1 c)
TAddC' a b T c => TAddC' (D1 a) (DE b) T (D0 c)
TAddC' a b F c => TAddC' (D1 a) (DD b) T (DF c)
TAddC' a b F c => TAddC' (D1 a) (DC b) T (DE c)
TAddC' a b F c => TAddC' (D1 a) (DB b) T (DD c)
TAddC' a b F c => TAddC' (D1 a) (DA b) T (DC c)
TAddC' a b F c => TAddC' (D1 a) (D9 b) T (DB c)
TAddC' a b F c => TAddC' (D1 a) (D8 b) T (DA c)
TAddC' a b F c => TAddC' (D1 a) (D7 b) T (D9 c)
TAddC' a b F c => TAddC' (D1 a) (D6 b) T (D8 c)
TAddC' a b F c => TAddC' (D1 a) (D5 b) T (D7 c)
TAddC' a b F c => TAddC' (D1 a) (D4 b) T (D6 c)
TAddC' a b F c => TAddC' (D1 a) (D3 b) T (D5 c)
TAddC' a b F c => TAddC' (D1 a) (D2 b) T (D4 c)
TAddC' a b F c => TAddC' (D1 a) (D1 b) T (D3 c)
TAddC' a b F c => TAddC' (D1 a) (D0 b) T (D2 c)
TAddC' a b T c => TAddC' (D0 a) (DF b) T (D0 c)
TAddC' a b F c => TAddC' (D0 a) (DE b) T (DF c)
TAddC' a b F c => TAddC' (D0 a) (DD b) T (DE c)
TAddC' a b F c => TAddC' (D0 a) (DC b) T (DD c)
TAddC' a b F c => TAddC' (D0 a) (DB b) T (DC c)
TAddC' a b F c => TAddC' (D0 a) (DA b) T (DB c)
TAddC' a b F c => TAddC' (D0 a) (D9 b) T (DA c)
TAddC' a b F c => TAddC' (D0 a) (D8 b) T (D9 c)
TAddC' a b F c => TAddC' (D0 a) (D7 b) T (D8 c)
TAddC' a b F c => TAddC' (D0 a) (D6 b) T (D7 c)
TAddC' a b F c => TAddC' (D0 a) (D5 b) T (D6 c)
TAddC' a b F c => TAddC' (D0 a) (D4 b) T (D5 c)
TAddC' a b F c => TAddC' (D0 a) (D3 b) T (D4 c)
TAddC' a b F c => TAddC' (D0 a) (D2 b) T (D3 c)
TAddC' a b F c => TAddC' (D0 a) (D1 b) T (D2 c)
TAddC' a b F c => TAddC' (D0 a) (D0 b) T (D1 c)

tT :: T Source

tF :: F Source

class TAnd a b c | a b -> cSource

Type-Level a and b = c

Instances

TAnd F F F
TAnd F T F
TAnd T F F
TAnd T T T
TAnd F (I b) F
TAnd F (O b) F
TAnd T (I b) (I b)
TAnd T (O b) (O b)
TAnd (I a) F F
TAnd (O a) F F
TAnd (I a) T (I a)
TAnd (O a) T (O a)
(TAnd a b c, TNF (O c) c') => TAnd (I a) (O b) c'
(TAnd a b c, TNF (I c) c') => TAnd (I a) (I b) c'
(TAnd a b c, TNF (O c) c') => TAnd (O a) (O b) c'
(TAnd a b c, TNF (O c) c') => TAnd (O a) (I b) c'

class TOr a b c | a b -> cSource

Type-Level a or b = c

Instances

TOr F F F
TOr F T T
TOr T F T
TOr T T T
TOr T (I b) T
TOr T (O b) T
TOr F (I b) (I b)
TOr F (O b) (O b)
TOr (I a) T T
TOr (O a) T T
TOr (I a) F (I a)
TOr (O a) F (I a)
(TOr a b c, TNF (I c) c') => TOr (I a) (O b) c'
(TOr a b c, TNF (I c) c') => TOr (I a) (I b) c'
(TOr a b c, TNF (O c) c') => TOr (O a) (O b) c'
(TOr a b c, TNF (I c) c') => TOr (O a) (I b) c'

class TNot a b | a -> b, b -> aSource

Type-Level: not a

Instances

TNot F T
TNot T F
TNot a b => TNot (I a) (O b)
TNot a b => TNot (O a) (I b)	TNot preserves normalization trivially
TNot a b => TNot (DF a) (D0 b)
TNot a b => TNot (DE a) (D1 b)
TNot a b => TNot (DD a) (D2 b)
TNot a b => TNot (DC a) (D3 b)
TNot a b => TNot (DB a) (D4 b)
TNot a b => TNot (DA a) (D5 b)
TNot a b => TNot (D9 a) (D6 b)
TNot a b => TNot (D8 a) (D7 b)
TNot a b => TNot (D7 a) (D8 b)
TNot a b => TNot (D6 a) (D9 b)
TNot a b => TNot (D5 a) (DA b)
TNot a b => TNot (D4 a) (DB b)
TNot a b => TNot (D3 a) (DC b)
TNot a b => TNot (D2 a) (DD b)
TNot a b => TNot (D1 a) (DE b)
TNot a b => TNot (D0 a) (DF b)

class (TXOr' a b c, TXOr' b c a, TXOr' c a b) => TXOr a b c | a b -> c, a c -> b, b c -> aSource

implemented this way rather than directly so that Binary can extend it properly. otherwise the normal form restriction makes that nigh impossible.

Instances

(TXOr' a b c, TXOr' b c a, TXOr' c a b) => TXOr a b c

class TXOr' a b c | a b -> cSource

Type-Level: a xor b = c

Instances

TXOr' F F F
TXOr' F T T
TXOr' T F T
TXOr' T T F
TXOr' F (I b) (I b)
TXOr' F (O b) (O b)
TNot b c => TXOr' T (I b) (O c)
TNot b c => TXOr' T (O b) (I c)
TNot b c => TXOr' (I b) T (O c)
TXOr' (I b) F (I b)
TNot b c => TXOr' (O b) T (I c)
TXOr' (O b) F (O b)
(TXOr' a b c, TNF (I c) c') => TXOr' (I a) (O b) c'
(TXOr' a b c, TNF (O c) c') => TXOr' (I a) (I b) c'
(TXOr' a b c, TNF (O c) c') => TXOr' (O a) (O b) c'
(TXOr' a b c, TNF (I c) c') => TXOr' (O a) (I b) c'

class TImplies a b c | a b -> cSource

Type-Level: a implies b = c

Instances

TImplies F F T
TImplies F T T
TImplies T F F
TImplies T T T
TImplies F (I b) T
TImplies F (O b) T
TImplies T (I b) (I b)
TImplies T (O b) (O b)
TImplies (I a) F T
TImplies (O a) F T
TImplies (I a) T (I a)
TImplies (O a) T (O a)
(TImplies a b c, TNF (I c) c') => TImplies (I a) (O b) c'
(TImplies a b c, TNF (I c) c') => TImplies (I a) (I b) c'
(TImplies a b c, TNF (O c) c') => TImplies (O a) (O b) c'
(TImplies a b c, TNF (I c) c') => TImplies (O a) (I b) c'

class TIf t x y z | t x y -> z whereSource

Type-Level: if t then x else y

Methods

tIf :: t -> x -> y -> zSource

Instances

TIf F x y y
TIf T x y x

tAnd :: TAnd a b c => a -> b -> cSource

tOr :: TOr a b c => a -> b -> cSource

tNot :: TNot a b => a -> bSource

tXOr :: TXOr a b c => a -> b -> cSource

tXOr' :: TXOr' a b c => a -> b -> cSource

tImplies :: TImplies a b c => a -> b -> cSource