source: src/utilities/option.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 461 bytes
Line 
1include "utilities/monad.ma".
2include "basics/types.ma".
3definition Option ≝ MakeMonad (mk_MonadDefinition
4  (* the monad *)
5  option
6  (* return *)
7  (λX.Some X)
8  (* bind *)
9  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
10  ???).
11//
12[(* bind_bind *)
13 #X#Y#Z*normalize //
14|(* bind_ret *)
15 #X*normalize //
16]
17qed.
18
19include "hints_declaration.ma".
20unification hint 0 ≔ X;
21M ≟ Option
22(*---------------*) ⊢
23option X ≡ monad (m_def M) X
24.
Note: See TracBrowser for help on using the repository browser.