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  

1  include "utilities/monad.ma". 

2  include "basics/types.ma". 

3  definition 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  ] 

17  qed. 

18  

19  include "hints_declaration.ma". 

20  unification hint 0 ≔ X; 

21  M ≟ Option 

22  (**) ⊢ 

23  option X ≡ monad (m_def M) X 

24  . 

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