Package option-map: The option map function

Information

nameoption-map
version1.14
descriptionThe option map function
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksum8d0c71b57363fe40b2f39dd3c3a510f1f9421c07
requiresbool
function
option-def
option-thm
showData.Bool
Data.Option
Function

Files

Defined Constant

Theorems

map id = id

f. map f none = none

f a. map f (some a) = some (f a)

f g. map f map g = map (f g)

f g x. map (f g) x = map f (map g x)

External Type Operators

External Constants

Assumptions

¬

t. t t

x. id x = x

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

x y. x = y y = x

x. x = none a. x = some a

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

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

f g x. (f g) x = f (g x)

f g. (x. f x = g x) f = g

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

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