Theory "state_option"

Parents pair option

Signature

Constant	Type
STATE_OPTION_BIND	:(α, β) state_option -> (β -> (α, γ) state_option) -> (α, γ) state_option
STATE_OPTION_FAIL	:(α, β) state_option
STATE_OPTION_IGNORE_BIND	:(α, β) state_option -> (α, γ) state_option -> (α, γ) state_option
STATE_OPTION_LIFT	:β option -> (α, β) state_option
STATE_OPTION_UNIT	:β -> (α, β) state_option

STATE_OPTION_FAIL_def

|- ∀s. STATE_OPTION_FAIL s = NONE

STATE_OPTION_UNIT_def

|- ∀a s. STATE_OPTION_UNIT a s = SOME (a,s)

STATE_OPTION_BIND_def

|- ∀m f s. STATE_OPTION_BIND m f s = OPTION_BIND (m s) (UNCURRY f)

STATE_OPTION_IGNORE_BIND_def

|- ∀m1 m2 s. STATE_OPTION_IGNORE_BIND m1 m2 s = OPTION_BIND (m1 s) (m2 o SND)

STATE_OPTION_LIFT_def

|- ∀m s. STATE_OPTION_LIFT m s = OPTION_BIND m (λa. SOME (a,s))