Last change
on this file since 2717 was
2717,
checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.
I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).
I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size:
539 bytes

Line  

1  open Preamble 

2  

3  open Jmeq 

4  

5  open Russell 

6  

7  open Bool 

8  

9  open Nat 

10  

11  open List 

12  

13  open Setoids 

14  

15  open Relations 

16  

17  open Hints_declaration 

18  

19  open Core_notation 

20  

21  open Pts 

22  

23  open Logic 

24  

25  open Types 

26  

27  open Monad 

28  

29  val state_monad : Monad.setoidMonadProps 

30  

31  val state_get : 'a1 Monad.smax_def__o__monad 

32  

33  val state_set : 'a1 > Types.unit0 Monad.smax_def__o__monad 

34  

35  val state_run : 'a1 > 'a2 Monad.smax_def__o__monad > 'a2 

36  

37  val state_update : ('a1 > 'a1) > Types.unit0 Monad.smax_def__o__monad 

38  

39  val state_pred : Monad.monadPred 

40  

41  val stateRel : Monad.monadRel 

42  

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