source: extracted/floats.mli @ 2620

Last change on this file since 2620 was 2620, checked in by campbell, 7 years ago

Sufficient hacking to run the extracted Clight semantics.

File size: 961 bytes
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Coqlib
30
31open Arithmetic
32
33open Char
34
35open String
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Extranat
44
45open Integers
46
47type float 
48(*
49val fzero : float
50
51val fone : float
52
53val fneg : float -> float
54
55val fabs : float -> float
56
57val singleoffloat : float -> float
58
59val intoffloat : Nat.nat -> float -> BitVector.bitVector
60
61val intuoffloat : Nat.nat -> float -> BitVector.bitVector
62
63val floatofint : Nat.nat -> BitVector.bitVector -> float
64
65val floatofintu : Nat.nat -> BitVector.bitVector -> float
66
67val fadd : float -> float -> float
68
69val fsub : float -> float -> float
70
71val fmul : float -> float -> float
72
73val fdiv : float -> float -> float
74
75val fcmp : Integers.comparison -> float -> float -> Bool.bool
76
77val eq_dec0 : float -> float -> (__, __) Types.sum
78*)
Note: See TracBrowser for help on using the repository browser.