source: driver/extracted/integers.mli @ 3106

Last change on this file since 3106 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: 3.0 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Jmeq
18
19open Russell
20
21open List
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Types
30
31open Extranat
32
33open Vector
34
35open Div_and_mod
36
37open Util
38
39open FoldStuff
40
41open BitVector
42
43open Exp
44
45open Arithmetic
46
47type comparison =
48| Ceq
49| Cne
50| Clt
51| Cle
52| Cgt
53| Cge
54
55val comparison_rect_Type4 :
56  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
57
58val comparison_rect_Type5 :
59  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
60
61val comparison_rect_Type3 :
62  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
63
64val comparison_rect_Type2 :
65  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
66
67val comparison_rect_Type1 :
68  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
69
70val comparison_rect_Type0 :
71  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
72
73val comparison_inv_rect_Type4 :
74  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
75  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
76
77val comparison_inv_rect_Type3 :
78  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
79  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
80
81val comparison_inv_rect_Type2 :
82  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
83  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
84
85val comparison_inv_rect_Type1 :
86  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
87  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
88
89val comparison_inv_rect_Type0 :
90  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
91  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
92
93val comparison_discr : comparison -> comparison -> __
94
95val comparison_jmdiscr : comparison -> comparison -> __
96
97val negate_comparison : comparison -> comparison
98
99val swap_comparison : comparison -> comparison
100
101val wordsize : Nat.nat
102
103type int = BitVector.bitVector
104
105val repr : Nat.nat -> int
106
107val zero : int
108
109val one : int
110
111val mone : BitVector.bitVector
112
113val iwordsize : int
114
115val eq_dec : int -> int -> (__, __) Types.sum
116
117val eq : int -> int -> Bool.bool
118
119val lt : int -> int -> Bool.bool
120
121val ltu : int -> int -> Bool.bool
122
123val neg : int -> int
124
125val mul :
126  BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector
127
128val zero_ext_n :
129  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
130
131val zero_ext : Nat.nat -> int -> int
132
133val sign_ext_n :
134  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
135
136val sign_ext : Nat.nat -> int -> int
137
138val i_and : int -> int -> int
139
140val or0 : int -> int -> int
141
142val xor : int -> int -> int
143
144val not : int -> int
145
146val shl : int -> int -> int
147
148val shru : int -> int -> int
149
150val shr : int -> int -> int
151
152val shrx : int -> int -> int
153
154val shr_carry : int -> int -> BitVector.bitVector
155
156val rol : int -> int -> int
157
158val ror : int -> int -> int
159
160val rolm : int -> int -> int -> int
161
162val cmp : comparison -> int -> int -> Bool.bool
163
164val cmpu : comparison -> int -> int -> Bool.bool
165
166val notbool : int -> int
167
Note: See TracBrowser for help on using the repository browser.