include "utilities/monad.ma".
include "basics/types.ma".

definition Option ≝ MakeMonadProps
  (* the monad *)
  option
  (* return *)
  (λX.Some X)
  (* bind *)
  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
  ???.
// #X[2:#Y#Z]*normalize//qed.

include "hints_declaration.ma".
unification hint 0 ≔ X;
N ≟ max_def Option, M ≟ m_def N
(*---------------*) ⊢
option X ≡ monad M X
.

definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝
λX,m,prf.match m return λx.m = x → X with
  [ Some t ⇒ λ_.t
  | None ⇒ λeq_m.?
  ] (refl …). elim (absurd … eq_m prf) qed.