source: extracted/frontend_misc.mli @ 2817

Last change on this file since 2817 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.2 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79open ClassifyOp
80
81open Events
82
83open Smallstep
84
85open Extra_bool
86
87open Values
88
89open FrontEndVal
90
91open Hide
92
93open ByteValues
94
95open Division
96
97open Z
98
99open BitVectorZ
100
101open Pointers
102
103open GenMem
104
105open FrontEndMem
106
107open Globalenvs
108
109open Csem
110
111open Star
112
113open IOMonad
114
115open IO
116
117open Sets
118
119open Listb
120
121val block_DeqSet : Deqsets.deqSet
122
123val mem_assoc_env :
124  AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool
125
126type 'a lset = 'a List.list
127
128val empty_lset : 'a1 List.list
129
130val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list
131
132val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list
133
134val lset_difference : Deqsets.deqSet -> __ lset -> __ lset -> __ List.list
135
136val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2
137
138val one_bv : Nat.nat -> BitVector.bitVector
139
140val ith_carry :
141  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
142  Bool.bool
143
144val ith_bit :
145  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
146  Bool.bool
147
148val bitvector_fold :
149  Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
150  Bool.bool) -> BitVector.bitVector
151
152val bitvector_fold2 :
153  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
154  BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
155  BitVector.bitVector
156
157val addition_n_direct :
158  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
159  BitVector.bitVector
160
161val increment_direct : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
162
163val twocomp_neg_direct :
164  Nat.nat -> BitVector.bitVector -> BitVector.bitVector
165
166val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool
167
Note: See TracBrowser for help on using the repository browser.