Fixed Github Issue #674: Nonstd build failing in projects/sat/proof-c…

…hecker-array

books/projects/sat/proof-checker-array/farray.lisp

@@ -47,7 +47,7 @@
 ;; ============================= LAYOUT ==============================
 
 ;; The layout of this book is as follows:
-;; -- Define the stobj in which the farray will reside.  
+;; -- Define the stobj in which the farray will reside.
 ;; -- Define and analyze recursive predicate for checking farray field table.
 ;; -- Define farray predicate.
 ;; -- Define types, accessors, and updaters including:
@@ -271,18 +271,18 @@
 (defthm sb60p-types
   (implies (sb60p x)
            (and (integerp x)
-                (rationalp x)
+                (real/rationalp x)
                 (acl2-numberp x))))
 
 ;; integerp implies other things.  Wish this could be removed...  Potentially
 ;; make this forward-chaining.
 (defthm integerp-types
   (implies (integerp x)
-           (and (rationalp x)
+           (and (real/rationalp x)
                 (acl2-numberp x))))
 
 ;; addition preserves integerp
-(local 
+(local
  (defthm integerp-+
    (implies (and (integerp i)
                  (integerp j))
@@ -373,7 +373,7 @@
    :rule-classes (:linear :rewrite)))
 
 ;; Field table entries are less than the length of mem.
-(local 
+(local
  (defthm field-tablep-implies-<-memi-mem-len
    (implies (and (field-tablep i end st)
                  ;; (integerp i)
@@ -430,7 +430,7 @@
    :rule-classes (:linear :rewrite)))
 
 ;; The field table is preserved when writes are above the table.
-(local 
+(local
  (defthm field-tablep-!memi
    (implies (and (field-tablep i end st)
                  ;; (integerp i)
@@ -565,7 +565,7 @@
                             (j (+ f start)))
                  (:instance sb60p-memi
                             (i (+ start 1 f)))))))
-                 
+
 ;; Each field fits inside mem.
 (defthm flength-<-mem-len
   (implies (and (farrayp start st)
@@ -626,7 +626,7 @@
                               (end (+ 1 start (memi start st))))))))))
 
 ;; Any field offset is within mem.
-(local 
+(local
  (defthm field-offsetp-implies-offset-+-index-<-mem-len
    (implies (and (field-offsetp offset f start st)
                  (farrayp start st)
@@ -804,7 +804,7 @@
 
 ;; Induct once to show that all fields less than k have entries less than k's
 ;; entry.
-(local 
+(local
  (defthm field-tablep-ordering-arbitrary-k
    (implies (and ;; (integerp i)
              ;; (<= 0 i)
@@ -857,7 +857,7 @@
 
 ;; Abstract the lemmas above to be based on fields instead of field table
 ;; entries.
-(local 
+(local
  (defthm field-tablep-ordering-arbitrary-field-based
    (implies (and (farrayp start st)
                  (fieldp f1 start st)
@@ -903,7 +903,7 @@
             :use ((:instance field-tablep-ordering-arbitrary-field-based-offset-one))))))
 
 ;; If two fields are distict, so are all offsets into those fields.
-(local 
+(local
  (defthm field-tablep-ordering-arbitrary-field-based-offset-both-ne
    (implies (and (farrayp start st)
                  (fieldp f1 start st)
@@ -1044,7 +1044,7 @@
            (equal (field-offsetp o1 f1 start (fwrite f2 o2 v start st))
                   (field-offsetp o1 f1 start st))))
 
-  
+
 
 
 ;; ============================ PRINTING =============================
@@ -1209,15 +1209,15 @@
 
 ;; ;; < implies !=
 ;; ;; Would like to remove without adding arithmetic.
-;; (local 
+;; (local
 ;;  (defthm <-implies-not-equal
 ;;    (implies (< x y)
 ;;             (not (equal x y)))
 ;;    :rule-classes :forward-chaining))
 
 ;; ;; < transitive
 ;; ;; Would like to remove without adding arithmetic.
-;; (local 
+;; (local
 ;;  (defthm <-transitive-fc
 ;;    (implies (and (< x y)
 ;;                  (< y z))
@@ -1429,7 +1429,7 @@
 ;;     0
 ;;     2
 ;;     7
-;;     8 
+;;     8
 ;;     11
 ;;     5
 ;;     1