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  

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 

48  (* 

49  val fzero : float 

50  

51  val fone : float 

52  

53  val fneg : float > float 

54  

55  val fabs : float > float 

56  

57  val singleoffloat : float > float 

58  

59  val intoffloat : Nat.nat > float > BitVector.bitVector 

60  

61  val intuoffloat : Nat.nat > float > BitVector.bitVector 

62  

63  val floatofint : Nat.nat > BitVector.bitVector > float 

64  

65  val floatofintu : Nat.nat > BitVector.bitVector > float 

66  

67  val fadd : float > float > float 

68  

69  val fsub : float > float > float 

70  

71  val fmul : float > float > float 

72  

73  val fdiv : float > float > float 

74  

75  val fcmp : Integers.comparison > float > float > Bool.bool 

76  

77  val eq_dec0 : float > float > (__, __) Types.sum 

78  *) 

Note: See
TracBrowser
for help on using the repository browser.