Package bool-def: Basic boolean definitions

Information

namebool-def
version1.4
descriptionBasic boolean definitions
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2011-07-20
showData.Bool

Files

Defined Constants

Theorems

F p. p

(~) = λp. p F

T (λp. p) = λp. p

() = λp. p = λx. T

() = λp q. p q p

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

() = λ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 T) x = t1) ((t F) x = t2)

Input Type Operators

Input Constants