Package option-dest: Theory of the option destructors

Information

nameoption-dest
version1.14
descriptionTheory of the option destructors
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.Option

Files

Defined Constants

Theorems

x. case.none.some none some x = x

(isNone none T) a. isNone (some a) F

(isSome none F) a. isSome (some a) T

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

Input Type Operators

Input Constants

Assumptions

T

() = λP. P ((select) P)

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

x. x = x T

() = λp q. p q p

x. x = none a. x = 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

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