Package unit-def: Definition of the unit type

Information

nameunit-def
version1.13
descriptionDefinition of the unit type
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-11-01
checksum5f6feb4c479325bbb29dd41bcf726dc252ee0910
requiresbool
showData.Bool
Data.Unit

Files

Defined Type Operator

Defined Constant

Theorem

v. v = ()

External Type Operators

External 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