Data.Type.Boolean

Portability	non-portable (FD and MPTC. no constructor data types)
Stability	experimental
Maintainer	Edward Kmett <ekmett@gmail.com>

Description

Simple closed type-level booleans.

Synopsis

class TCBool Closure x => TBool x

data F

data T

tT :: T

tF :: F

class TAnd a b c | a b -> c

class TOr a b c | a b -> c

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

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

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

class TImplies a b c | a b -> c

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

tIf :: t -> x -> y -> z

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

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

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

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

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

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

tIf :: TIf t x y z => t -> x -> y -> z

Documentation

class TCBool Closure x => TBool x

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

Instances

TBool F

TBool T

data F

Instances

TCBinary Closure F

TCBool Closure F

TEven F T

TEven T F

THex2Binary' F F

TNot F T

TNot T F

TSucc T F

Trichotomy F SignZero

LSB F F F

LSN F H0 F

SHR1 H0 F F

TAnd F F F

TAnd F T F

TAnd T F F

TCountBits' F F F

TEq F F T

TEq F T F

TEq T F F

TImplies F F T

TImplies F T T

TImplies T F F

TMul a F F

TNF' F F F

TNF' T T F

TOr F F F

TOr F T T

TOr T F T

TShift' F F F

TShift' F T F

TShift' T F T

TXOr' F F F

TXOr' F T T

TXOr' T F T

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

TIf F x y y

TAddC' F F T (D1 F)

TAddC' F F T (I F)

TAddC' T T F (DE T)

TAddC' T T F (O T)

SHR1 H1 F (D1 F)

TPow a F (I F)

TPow' a F (D1 F)

TSucc F (D1 F)

TSucc F (I F)

TAnd F (I b) F

TAnd F (O b) F

TImplies F (I b) T

TImplies F (O b) T

TSucc a b => TAddC' F (DF a) T (D0 b)

TAddC' F (I a) F (I a)

TSucc a b => TAddC' F (I a) T (O b)

TAddC' F (O a) F (O a)

TAddC' F (O a) T (I a)

TSucc b a => TAddC' T (D0 a) F (DF b)

TAddC' T (I a) F (O a)

TSucc b a => TAddC' T (O a) F (I b)

TOr F (I b) (I b)

TOr F (O b) (O b)

TXOr' F (I b) (I b)

TXOr' F (O b) (O b)

Trichotomy (I F) Positive

LSB (I F) T F

LSB (O T) F T

TAnd (I a) F F

TAnd (O a) F F

(TCountBits' a n F, TSucc n m) => TCountBits' (I a) m F

TCountBits' a n F => TCountBits' (O a) n F

TEq (I m) F F

TEq (I m) T F

TEq (O m) F F

TEq (O m) T F

TImplies (I a) F T

TImplies (O a) F T

TNF' (D0 F) F F

TNF' (DF T) T F

TNF' (I T) T F

TNF' (O F) F F

LSB (O a) F a => X (O a) F a

TSucc b a => TAddC' (D0 a) T F (DF b)

TSucc a b => TAddC' (DF a) F T (D0 b)

TAddC' (I a) F F (I a)

TSucc a b => TAddC' (I a) F T (O b)

TAddC' (I a) T F (O a)

TAddC' (O a) F F (O a)

TAddC' (O a) F T (I a)

TSucc b a => TAddC' (O a) T F (I b)

LSB (O (I n)) F (I n)

LSB (O (O n)) F (O n)

TOr (I a) F (I a)

TOr (O a) F (I a)

TShift' (I a) F (I a)

TShift' (O a) F (O a)

TXOr' (I b) F (I b)

TXOr' (O b) F (O b)

TEq (I m) (O n) F

TEq (O m) (I n) F

TNF' (I F) (I 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)

data T

Instances

TCBinary Closure T

TCBool Closure T

TEven F T

TEven T F

THex2Binary' T T

TNot F T

TNot T F

TSucc T F

Trichotomy T Negative

LSB T T T

LSN T HF T

TAnd F T F

TAnd T F F

TAnd T T T

TCountBits' T T T

TEq F F T

TEq F T F

TEq T F F

TEq T T T

TImplies F F T

TImplies F T T

TImplies T F F

TImplies T T T

TNeg a b => TMul a T b

TNF' T T F

TOr F T T

TOr T F T

TOr T T T

TShift' F T F

TShift' T F T

TShift' T T T

TXOr' F T T

TXOr' T F T

TXOr' T T F

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

TIf T x y x

TAddC' F F T (D1 F)

TAddC' F F T (I F)

TAddC' T T F (DE T)

TAddC' T T F (O T)

SHR1 H0 T (DE T)

SHR1 H1 T (DE T)

TImplies F (I b) T

TImplies F (O b) T

TOr T (I b) T

TOr T (O b) T

TSucc a b => TAddC' F (DF a) T (D0 b)

TSucc a b => TAddC' F (I a) T (O b)

TAddC' F (O a) T (I a)

TSucc b a => TAddC' T (D0 a) F (DF b)

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)

TAnd T (I b) (I b)

TAnd T (O b) (O b)

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)

TSucc (DE T) T

TSucc (O T) T

Trichotomy (O T) Negative

LSB (I F) T F

LSB (O T) F T

TCountBits' a m F => TCountBits' (I a) m T

(TCountBits' a n F, TSucc m n) => TCountBits' (O a) n T

TEq (I m) T F

TEq (O m) T F

TImplies (I a) F T

TImplies (O a) F T

TNF' (DF T) T F

TNF' (I T) T F

TOr (I a) T T

TOr (O a) T T

TShift' (I a) T a

TShift' (O a) T a

LSB (I a) T a => X (I a) T a

TSucc b a => TAddC' (D0 a) T F (DF b)

TSucc a b => TAddC' (DF a) F T (D0 b)

TSucc a b => TAddC' (I a) F T (O b)

TAddC' (I a) T F (O a)

TAddC' (I a) T T (I a)

TAddC' (O a) F T (I a)

TSucc b a => TAddC' (O a) T F (I b)

TAddC' (O a) T T (O a)

LSB (I (I n)) T (I n)

LSB (I (O n)) T (O n)

TAnd (I a) T (I a)

TAnd (O a) T (O 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)

TNF' (I F) (I F) T

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

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

TNF' (O T) (O 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)

tT :: T

tF :: F

class TAnd a b c | a b -> c

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 (I c) c') => TAnd (I a) (I b) c'

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

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

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

class TOr a b c | a b -> c

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) (I b) c'

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

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

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

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

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)

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

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

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)

TXOr' (I b) F (I b)

TNot b c => TXOr' (I b) T (O c)

TXOr' (O b) F (O b)

TNot b c => TXOr' (O b) T (I c)

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

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

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

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

class TImplies a b c | a b -> c

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) (I b) c'

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

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

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

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

Type-Level: if t then x else y

Methods

tIf :: t -> x -> y -> z

Instances

TIf F x y y

TIf T x y x

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

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

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

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

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

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

tIf :: TIf t x y z => t -> x -> y -> z

Produced by Haddock version 0.8