Package bool-def: Boolean definitions

Information

namebool-def
version1.11
descriptionBoolean definitions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2014-11-17
checksum0a4ed62119c317adca068ae0550c03a7c636698c
showData.Bool

Files

Defined Constants

Theorems

p. p

(¬) = λp. p

(λp. p) = λp. p

() = λp. p = λx.

() = λp q. p q p

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

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

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

(∃!) = λp. () p x y. p x p y x = y

cond = λt t1 t2. select x. ((t ) x = t1) ((t ) x = t2)

External Type Operators

External Constants