Filtering...

1d-arr

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

Included Books

1d-arr
other
(in-package "ACL2")
include-book
(include-book "../1d-arr")
widgp-of-widg-fixencapsulate
(encapsulate nil
  (defund widgp
    (x)
    (declare (xargs :guard t))
    (eq x 'the-default-widg))
  (defund widg-fix
    (x)
    (declare (xargs :guard t))
    (if (widgp x)
      x
      'the-default-widg))
  (local (in-theory (enable widg-fix)))
  (defthm widgp-of-widg-fix (widgp (widg-fix x)))
  (defthm widg-fix-when-widgp
    (implies (widgp x) (equal (widg-fix x) x))))
other
(def-1d-arr widgarr
  :slotname widg
  :pred widgp
  :fix widg-fix
  :type-decl (satisfies widgp)
  :default-val the-default-widg)
swidg-fix-when-swidgpencapsulate
(encapsulate nil
  (defund swidgp (x) (declare (xargs :guard t)) (symbolp x))
  (defund swidg-fix
    (x)
    (declare (xargs :guard t))
    (if (swidgp x)
      x
      'the-default-swidg))
  (local (in-theory (enable swidg-fix)))
  (defthm swidg-fix-when-swidgp
    (implies (swidgp x) (equal (swidg-fix x) x))))
other
(def-1d-arr swidgarr
  :slotname swidg
  :pred swidgp
  :fix swidg-fix
  :type-decl (and symbol (satisfies swidgp))
  :pkg-sym asdfs
  :default-val the-default-swidg)
other
(def-1d-arr swidgarr2
  :slotname swidg2
  :pred swidgp
  :fix swidg-fix
  :type-decl (and symbol (satisfies swidgp))
  :pkg-sym asdfs
  :default-val the-default-swidg2)
other
(def-1d-arr objarr :slotname obj :default-val asdfa)
other
(def-1d-arr swidgarr3
  :slotname swidg3
  :pred swidgp
  :type-decl (and symbol (satisfies swidgp))
  :pkg-sym asdfs
  :default-val the-default-swidg2)