Last change
on this file since 1812 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

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.