Filtering...

natarr

books/std/stobjs/natarr

Included Books

1d-arr nats-equiv top equiv arith-equivs nat-listp
other
(in-package "ACL2")
include-book
(include-book "1d-arr")
include-book
(include-book "std/lists/nats-equiv" :dir :system)
local
(local (include-book "arithmetic/top" :dir :system))
local
(local (include-book "std/lists/equiv" :dir :system))
local
(local (include-book "std/basic/arith-equivs" :dir :system))
local
(local (include-book "std/typed-lists/nat-listp" :dir :system))
other
(def-1d-arr natarr
  :slotname nat
  :pred natp
  :fix nfix
  :type-decl (integer 0 *)
  :default-val 0
  :parents (std/stobjs))