Filtering...

2d-arr

books/std/stobjs/tests/2d-arr

Included Books

2d-arr resize-list
other
(in-package "ACL2")
include-book
(include-book "../2d-arr")
local
(local (include-book "std/lists/resize-list" :dir :system))
other
(def-2d-arr intmatrix
  :prefix imx
  :pred integerp
  :type-decl integer
  :default-val 0
  :fix ifix)
f-stringpfunction
(defun f-stringp
  (x)
  (declare (xargs :guard t))
  (and (stringp x) (< 0 (length x)) (eql (char x 0) #\f)))
nonempty-str-fixfunction
(defun nonempty-str-fix
  (x)
  (declare (xargs :guard t))
  (if (and (stringp x) (< 0 (length x)))
    x
    "f"))
f-stringp-when-stringptheorem
(defthm f-stringp-when-stringp
  (implies (and (stringp x) (< 0 (length x)) (equal (char x 0) #\f))
    (f-stringp x)))
nonempty-str-fix-when-f-stringptheorem
(defthm nonempty-str-fix-when-f-stringp
  (implies (f-stringp x) (equal (nonempty-str-fix x) x)))
in-theory
(in-theory (disable f-stringp nonempty-str-fix))
other
(def-2d-arr fstring2d
  :prefix fs2d
  :pred (lambda (x) (and (stringp x) (f-stringp x)))
  :type-decl (and string (satisfies f-stringp))
  :fix nonempty-str-fix
  :default-val "f")
other
(def-2d-arr s61v
  :pred (lambda (x) (signed-byte-p 61 x))
  :type-decl (signed-byte 61)
  :default-val 0
  :fix ifix
  :elt-guard (integerp x)
  :elt-okp (and (<= x (1- (expt 2 60))) (<= (- (expt 2 60)) x)))
other
(define test-s61v
  ((elt integerp) s61v)
  (let* ((s61v (s61v-resize-rows 5 s61v)) (s61v (s61v-resize-cols 4 s61v))
      (s61v (s61v-set2 0 0 elt s61v)))
    s61v))