Last change
on this file since 1812 was
1635,
checked in by tranquil, 9 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:
903 bytes

Line  

1  include "utilities/monad.ma". 

2  include "basics/types.ma". 

3  include "basics/lists/list.ma". 

4  definition Trace ≝ λT : Type[0].MakeMonad (mk_MonadDefinition 

5  (* the monad *) 

6  (λX.X × (list T)) 

7  (* return *) 

8  (λX,x.〈x, [ ]〉) 

9  (* bind *) 

10  (λX,Y,m,f. let 〈x, ts〉 ≝ m in let 〈y,ts'〉 ≝ f x in 〈y, ts @ ts'〉) 

11  ???). 

12  [(* bind_bind *) 

13  #X#Y#Z*#x#t1#f#g 

14  normalize elim (f x) 

15  #y#t2 normalize elim (g y) 

16  #z#t3 normalize >associative_append // 

17  (* bind_ret *) 

18  #X*#x#t normalize >append_nil // 

19  (* ret_bind *) 

20  #X#Y#x#f normalize elim (f x) #y #t' normalize // 

21  ] 

22  qed. 

23  

24  include "hints_declaration.ma". 

25  unification hint 0 ≔ X, T; 

26  M ≟ Trace T 

27  (**) ⊢ 

28  X × (list T) ≡ monad (m_def M) X 

29  . 

30  

31  definition trace_emit : ∀T. T → monad (Trace T) unit ≝ 

32  λT,t.〈it, [t]〉. 

33  

34  definition trace_emits : ∀T. list T → monad (Trace T) unit ≝ 

35  λT,ts.〈it, ts〉. 

36  

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