Package unit-def: Definition of the unit type

Information

nameunit-def
version1.8
descriptionDefinition of the unit type
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-12-18
requiresbool
showData.Bool
Data.Unit

Files

Defined Type Operator

Defined Constant

Theorem

v. v = ()

Input Type Operators

Input Constants

Assumptions

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

t. (x. t) t

() = λp. p = λx.

t. (t ) t

() = λp q. p q p

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

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