~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/top/top.lisp

• browse files at revision 7
• compare with another revision
• download diff
• download tarball
• view history from revision 7

Show diffs side-by-side

added

removed

books/rtl/rel6/support/top/top.lisp

 

1

(in-package "ACL2")

 

2

 

 

3

(set-enforce-redundancy t)

 

4

 

 

5

; Optionally, one may wish to consider:

 

6

; (include-book "../../../misc/rtl-untranslate")

 

7

; to inhibit expansion of macros in proof output.

 

8

 

 

9

; We deliberately exclude any *-helpers.lisp books that may appear here.

 

10

 

 

11

(include-book "../lib1/rtl") ;semantics of the basic RTL primitives

 

12

 

 

13

(include-book "../lib1/rtlarr") ;semantics RTL array primitives

 

14

 

 

15

(include-book "../lib1/basic") ;properties of basic arithmetic functions: floor, ceiling, 

 

16

;                       exponential, and remainder

 

17

 

 

18

(include-book "../lib1/bits") ;bit vectors

 

19

 

 

20

(include-book "../lib1/log") ;logical operations

 

21

 

 

22

(include-book "../lib1.delta1/float") ;floating-point numbers

 

23

 

 

24

(include-book "../lib1/reps") ;floating-point formats and representations

 

25

 

 

26

(include-book "../lib1.delta1/round") ;floating-point rounding

 

27

 

 

28

(include-book "../lib1/add") ;support for reasoning about floating-point addition

 

29

;                      (leading one prediction and sticky bit computation)

 

30

 

 

31

; Users may prefer to replace the (include-book "arith") below with:

 

32

; (include-book "../arithmetic/top")

 

33

 

 

34

(include-book "../lib1.delta1/mult")  ; integerp multiplier

 

35

 

 

36

(include-book "../lib1/arith") ;general arithmetic package

 

37

 

 

38

(include-book "../lib1/util") ;misc helpful stuff including a few macros

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1