source: extracted/deqsets_extras.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: 314 bytes
Line 
1open Preamble
2
3open Relations
4
5open Bool
6
7open Hints_declaration
8
9open Core_notation
10
11open Pts
12
13open Logic
14
15open Types
16
17open Deqsets
18
19open Sets
20
21open Nat
22
23open List
24
25open Listb
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open Util
34
35val eqb_elim :
36  Deqsets.deqSet -> __ -> __ -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
37
Note: See TracBrowser for help on using the repository browser.