Last change
on this file since 1681 was
1647,
checked in by tranquil, 10 years ago

 corrected some notation problems
 adapted Cligth with slight modifications to new monad framework

File size:
614 bytes

Line  

1  include "utilities/monad.ma". 

2  include "basics/types.ma". 

3  

4  definition 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  

14  include "hints_declaration.ma". 

15  unification hint 0 ≔ X; 

16  N ≟ max_def Option, M ≟ m_def N 

17  (**) ⊢ 

18  option X ≡ monad M X 

19  . 

20  

21  definition 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.