source: src/utilities/option.ma @ 1640

Last change on this file since 1640 was 1640, checked in by tranquil, 9 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 pre-fork material
File size: 1.3 KB
Line 
1include "utilities/monad.ma".
2include "basics/types.ma".
3
4definition 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
14include "hints_declaration.ma".
15unification hint 0 ≔ X;
16M ≟ m_def Option
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.
26
27(* playground for notation problems *)
28
29inductive option_bis (X : Type[0]) : Type[0] ≝
30| Some' : X → option_bis X
31| None' : option_bis X.
32
33definition option_to_option' ≝ λX.λm : option X. match m with [ Some x ⇒ Some' ? x | None ⇒ None' ?].
34
35coercion o_to_o' : ∀X.∀m : option X. option_bis X ≝ option_to_option'
36  on _m : option ? to option_bis ?.
37 
38
39definition 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
46unification hint 0 ≔ X ;
47M ≟ m_def Option_bis
48(*---------------*) ⊢
49option_bis X ≡ monad M X
50.
51
52(* does not typecheck
53check (λX.λm : option_bis X.λn : option X.! x ← n ; m)
54*)
Note: See TracBrowser for help on using the repository browser.