source: src/utilities/option.ma @ 1651

Last change on this file since 1651 was 1647, checked in by tranquil, 8 years ago
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File size: 614 bytes
Line 
1include "utilities/monad.ma".
2include "basics/types.ma".
3
4definition Option ≝ MakeMonadProps
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 ?])
11  ???.
12// #X[2:#Y#Z]*normalize//qed.
13
14include "hints_declaration.ma".
15unification hint 0 ≔ X;
16N ≟ max_def Option, M ≟ m_def N
17(*---------------*) ⊢
18option X ≡ monad M X
19.
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.?
25  ] (refl …). elim (absurd … eq_m prf) qed.
Note: See TracBrowser for help on using the repository browser.