source: extracted/state.mli @ 2717

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 
1open Preamble
2
3open Jmeq
4
5open Russell
6
7open Bool
8
9open Nat
10
11open List
12
13open Setoids
14
15open Relations
16
17open Hints_declaration
18
19open Core_notation
20
21open Pts
22
23open Logic
24
25open Types
26
27open Monad
28
29val state_monad : Monad.setoidMonadProps
30
31val state_get : 'a1 Monad.smax_def__o__monad
32
33val state_set : 'a1 -> Types.unit0 Monad.smax_def__o__monad
34
35val state_run : 'a1 -> 'a2 Monad.smax_def__o__monad -> 'a2
36
37val state_update : ('a1 -> 'a1) -> Types.unit0 Monad.smax_def__o__monad
38
39val state_pred : Monad.monadPred
40
41val stateRel : Monad.monadRel
42
Note: See TracBrowser for help on using the repository browser.