Package unit: The unit type

Information

nameunit
version1.21
descriptionThe unit type
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksum098b2cf5bceac9960544b90b9747f4d175bf0fc9
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

p. (x. p x) p ()

p. (x. p x) p ()

External Type Operators

External Constants

Assumptions

¬

¬

t. t t

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

t. (x. t) t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t t

t. ( t) ¬t

() = λp q. p q p

t. (t ) (t )

x y. x = y y = x

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

p. ¬(x. p x) x. ¬p x

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

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

() = λp q. r. (p r) (q r) r

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