Package unit-def: Definition of the unit type

Information

nameunit-def
version1.4
descriptionDefinition of the unit type
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
requiresbool
showData.Bool

Files

Defined Type Operator

Defined Constant

Theorem

v. v = Data.Unit.()

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

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