Last change
on this file since 2731 was
2717,
checked in by sacerdot, 8 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

Rev  Line  

[2717]  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.