1 | open Preamble |
---|

2 | |
---|

3 | open Div_and_mod |
---|

4 | |
---|

5 | open Jmeq |
---|

6 | |
---|

7 | open Russell |
---|

8 | |
---|

9 | open Util |
---|

10 | |
---|

11 | open Bool |
---|

12 | |
---|

13 | open Relations |
---|

14 | |
---|

15 | open Nat |
---|

16 | |
---|

17 | open List |
---|

18 | |
---|

19 | open Hints_declaration |
---|

20 | |
---|

21 | open Core_notation |
---|

22 | |
---|

23 | open Pts |
---|

24 | |
---|

25 | open Logic |
---|

26 | |
---|

27 | open Types |
---|

28 | |
---|

29 | open Coqlib |
---|

30 | |
---|

31 | open Arithmetic |
---|

32 | |
---|

33 | open Char |
---|

34 | |
---|

35 | open String |
---|

36 | |
---|

37 | open Vector |
---|

38 | |
---|

39 | open FoldStuff |
---|

40 | |
---|

41 | open BitVector |
---|

42 | |
---|

43 | open Extranat |
---|

44 | |
---|

45 | open Integers |
---|

46 | |
---|

47 | type float (* AXIOM TO BE REALIZED *) |
---|

48 | (* |
---|

49 | (** val fzero : float **) |
---|

50 | let fzero = |
---|

51 | failwith "AXIOM TO BE REALIZED" |
---|

52 | |
---|

53 | (** val fone : float **) |
---|

54 | let fone = |
---|

55 | failwith "AXIOM TO BE REALIZED" |
---|

56 | |
---|

57 | (** val fneg : float -> float **) |
---|

58 | let fneg = |
---|

59 | failwith "AXIOM TO BE REALIZED" |
---|

60 | |
---|

61 | (** val fabs : float -> float **) |
---|

62 | let fabs = |
---|

63 | failwith "AXIOM TO BE REALIZED" |
---|

64 | |
---|

65 | (** val singleoffloat : float -> float **) |
---|

66 | let singleoffloat = |
---|

67 | failwith "AXIOM TO BE REALIZED" |
---|

68 | |
---|

69 | (** val intoffloat : Nat.nat -> float -> BitVector.bitVector **) |
---|

70 | let intoffloat = |
---|

71 | failwith "AXIOM TO BE REALIZED" |
---|

72 | |
---|

73 | (** val intuoffloat : Nat.nat -> float -> BitVector.bitVector **) |
---|

74 | let intuoffloat = |
---|

75 | failwith "AXIOM TO BE REALIZED" |
---|

76 | |
---|

77 | (** val floatofint : Nat.nat -> BitVector.bitVector -> float **) |
---|

78 | let floatofint = |
---|

79 | failwith "AXIOM TO BE REALIZED" |
---|

80 | |
---|

81 | (** val floatofintu : Nat.nat -> BitVector.bitVector -> float **) |
---|

82 | let floatofintu = |
---|

83 | failwith "AXIOM TO BE REALIZED" |
---|

84 | |
---|

85 | (** val fadd : float -> float -> float **) |
---|

86 | let fadd = |
---|

87 | failwith "AXIOM TO BE REALIZED" |
---|

88 | |
---|

89 | (** val fsub : float -> float -> float **) |
---|

90 | let fsub = |
---|

91 | failwith "AXIOM TO BE REALIZED" |
---|

92 | |
---|

93 | (** val fmul : float -> float -> float **) |
---|

94 | let fmul = |
---|

95 | failwith "AXIOM TO BE REALIZED" |
---|

96 | |
---|

97 | (** val fdiv : float -> float -> float **) |
---|

98 | let fdiv = |
---|

99 | failwith "AXIOM TO BE REALIZED" |
---|

100 | |
---|

101 | (** val fcmp : Integers.comparison -> float -> float -> Bool.bool **) |
---|

102 | let fcmp = |
---|

103 | failwith "AXIOM TO BE REALIZED" |
---|

104 | |
---|

105 | (** val eq_dec0 : float -> float -> (__, __) Types.sum **) |
---|

106 | let eq_dec0 = |
---|

107 | failwith "AXIOM TO BE REALIZED" |
---|

108 | *) |
---|