Last change
on this file since 1640 was
1640,
checked in by tranquil, 8 years ago

 finished fork of semantics.ma
 unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the prefork material

File size:
1.3 KB

Line  

1  include "utilities/monad.ma". 

2  include "basics/types.ma". 

3  

4  definition Option ≝ MakeMonad (mk_MonadDefinition 

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[#Y#Z]*normalize//qed. 

13  

14  include "hints_declaration.ma". 

15  unification hint 0 ≔ X; 

16  M ≟ m_def Option 

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. 

26  

27  (* playground for notation problems *) 

28  

29  inductive option_bis (X : Type[0]) : Type[0] ≝ 

30   Some' : X → option_bis X 

31   None' : option_bis X. 

32  

33  definition option_to_option' ≝ λX.λm : option X. match m with [ Some x ⇒ Some' ? x  None ⇒ None' ?]. 

34  

35  coercion o_to_o' : ∀X.∀m : option X. option_bis X ≝ option_to_option' 

36  on _m : option ? to option_bis ?. 

37  

38  

39  definition Option_bis ≝ MakeMonad (mk_MonadDefinition 

40  option_bis 

41  (λX.Some' X) 

42  (λX,Y,m,f.match m with [Some' x ⇒ f x  None' ⇒ None' ?]) 

43  ???). // 

44  #X[#Y#Z] * normalize // qed. 

45  

46  unification hint 0 ≔ X ; 

47  M ≟ m_def Option_bis 

48  (**) ⊢ 

49  option_bis X ≡ monad M X 

50  . 

51  

52  (* does not typecheck 

53  check (λX.λm : option_bis X.λn : option X.! x ← n ; m) 

54  *) 

Note: See
TracBrowser
for help on using the repository browser.