Package option-dest-def: Definition of the option destructors

Information

nameoption-dest-def
version1.0
descriptionDefinition of the option destructors
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-02-19
showData.Bool

Files

Defined Constant

Theorem

(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

Input Type Operators

Input Constants

Assumptions

T

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

NONE' SOME'.
    fn.
      fn Data.Option.none = NONE' a. fn (Data.Option.some a) = SOME' a