include "basics/types.ma".

definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].