other
(in-package "STOBJS")
other
(include-book "../def-hash")
other
(include-book "centaur/fty/deftypes" :dir :system)
other
(include-book "centaur/fty/basetypes" :dir :system)
other
(def-hash basehash)
other
(def-hash basehashfix :alist-fix alist-fix)
other
(defmap symbol-key-alist :key-type symbolp)
other
(def-hash symkeyhash :alistp symbol-key-alist-p :key-p symbolp :hash-test eq)
other
(def-hash symkeyhashfix :alistp symbol-key-alist-p :alist-fix symbol-key-alist-fix :key-p symbolp :hash-test eq)
other
(def-hash symkeyhashkeyfix :alistp symbol-key-alist-p :key-p symbolp :key-fix symbol-fix :hash-test eq)
other
(def-hash symkeyhashfixkeyfix :alistp symbol-key-alist-p :alist-fix symbol-key-alist-fix :key-p symbolp :key-fix symbol-fix :hash-test eq)
other
(defmap symbol-key-alisttr :key-type symbolp :true-listp t)
other
(def-hash symkeytrhash :alistp symbol-key-alisttr-p :key-p symbolp :hash-test eq)
other
(def-hash symkeytrhashfix :alistp symbol-key-alisttr-p :alist-fix symbol-key-alisttr-fix :key-p symbolp :hash-test eq)
other
(def-hash symkeytrhashkeyfix :alistp symbol-key-alisttr-p :key-p symbolp :key-fix symbol-fix :hash-test eq)
other
(def-hash symkeytrhashfixkeyfix :alistp symbol-key-alisttr-p :alist-fix symbol-key-alisttr-fix :key-p symbolp :key-fix symbol-fix :hash-test eq)
other
(defmap integer-val-alist :val-type integerp)
other
(def-hash intvalhash :alistp integer-val-alist-p :val-p integerp :default-val (+ 1 2) :type-decl integer)
other
(def-hash intvalhashfix :alistp integer-val-alist-p :alist-fix integer-val-alist-fix :val-p integerp :default-val (+ 1 2) :type-decl integer)
other
(def-hash intvalhashkeyfix :alistp integer-val-alist-p :val-p integerp :val-fix ifix :default-val (+ 1 2) :type-decl integer)
other
(def-hash intvalhashfixkeyfix :alistp integer-val-alist-p :alist-fix integer-val-alist-fix :val-p integerp :val-fix ifix :default-val (+ 1 2) :type-decl integer)
other
(def-hash intnathash :alistp int-nat-alist-p :key-p integerp :val-p natp :hash-test eql :default-val (+ 1 2) :type-decl (integer 0 *))
other
(def-hash intnathashfix :alistp int-nat-alist-p :alist-fix int-nat-alist-fix :key-p integerp :val-p natp :hash-test eql :default-val (+ 1 2) :type-decl (integer 0 *))
other
(def-hash intnathashkeyfix :alistp int-nat-alist-p :key-p integerp :key-fix ifix :val-p natp :hash-test eql :default-val (+ 1 2) :type-decl (integer 0 *))