Package option-map-thm: Properties of the option map function

Information

nameoption-map-thm
version1.14
descriptionProperties of the option map function
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-01
checksum7622c09c1033bee20370b9a954302612ad1ddc74
requiresbool
function
option-map-def
option-thm
showData.Bool
Data.Option
Function

Files

Theorems

map id = id

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

t. (x. t) t

() = λp. p = λx.

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

f. map f none = none

t. t ¬t

() = λp q. p q p

t. (t ) (t )

x y. x = y y = x

x. x = none a. x = some a

f a. map f (some a) = some (f 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