3
(set-enforce-redundancy t)
5
; Optionally, one may wish to consider:
6
; (include-book "../../../misc/rtl-untranslate")
7
; to inhibit expansion of macros in proof output.
9
; We deliberately exclude any *-helpers.lisp books that may appear here.
11
(include-book "rtl") ;semantics of the basic RTL primitives
13
(include-book "rtlarr") ;semantics RTL array primitives
15
(include-book "basic") ;properties of basic arithmetic functions: floor, ceiling,
16
; exponential, and remainder
18
(include-book "bits") ;bit vectors
20
(include-book "log") ;logical operations
22
(include-book "float") ;floating-point numbers
24
(include-book "reps") ;floating-point formats and representations
26
(include-book "round") ;floating-point rounding
28
(include-book "add") ;support for reasoning about floating-point addition
29
; (leading one prediction and sticky bit computation)
31
; Users may prefer to replace the (include-book "arith") below with:
32
; (include-book "../../arithmetic/top")
33
(include-book "arith") ;general arithmetic package
35
(include-book "util") ;misc helpful stuff including a few macros