Package option-dest-thm: option-dest-thm

Information

nameoption-dest-thm
version1.3
descriptionoption-dest-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-09-21
showData.Bool

Files

Theorem

x. Data.Option.case Data.Option.none Data.Option.some x = x

Input Type Operators

Input Constants

Assumptions

T

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

x. x = x T

() = λp q. p q p

x. x = Data.Option.none a. x = Data.Option.some a

() = λ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

(b f. Data.Option.case b f Data.Option.none = b)
  b f a. Data.Option.case b f (Data.Option.some a) = f a