Package unit: The unit type

Information

nameunit
version1.12
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

t. t t

() = λp. p ((select) p)

t. (x. t) t

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

t. (t T) t

t. T t t

() = λp q. p q p

x y. x = y y = x

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

() = λp. q. (x. p x q) q

f g. (x. f x = g x) f = g

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