Package unit: The unit type

Information

nameunit
version1.6
descriptionThe unit type
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
showData.Bool
Data.Unit

Files

Defined Type Operator

Defined Constant

Theorems

v. v = ()

f g. f = g

e. fn. fn () = e

e. ∃!fn. fn () = e

P. P () x. P x

Input Type Operators

Input Constants

Assumptions

T

() = λP. P ((select) P)

t. (x. t) t

() = λp. p = λx. T

x. x = x T

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f T T

() = λP. q. (x. P x q) q

f g. f = g x. f x = g x

P. (∃!x. P x) (x. P x) x x'. P x P x' x = x'

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)