source: src/utilities/option.ma @ 1681

Last change on this file since 1681 was 1647, checked in by tranquil, 9 years ago
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File size: 614 bytes
RevLine 
[1635]1include "utilities/monad.ma".
2include "basics/types.ma".
[1640]3
[1647]4definition Option ≝ MakeMonadProps
[1635]5  (* the monad *)
6  option
7  (* return *)
8  (λX.Some X)
9  (* bind *)
10  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
[1647]11  ???.
12// #X[2:#Y#Z]*normalize//qed.
[1635]13
14include "hints_declaration.ma".
15unification hint 0 ≔ X;
[1647]16N ≟ max_def Option, M ≟ m_def N
[1635]17(*---------------*) ⊢
[1640]18option X ≡ monad M X
[1635]19.
[1640]20
21definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝
22λX,m,prf.match m return λx.m = x → X with
23  [ Some t ⇒ λ_.t
24  | None ⇒ λeq_m.?
[1647]25  ] (refl …). elim (absurd … eq_m prf) qed.
Note: See TracBrowser for help on using the repository browser.