Filtering...

acl2s-sigs

books/acl2s/acl2s-sigs
other
(in-package "ACL2S")
other
(include-book "base-theory" :ttags :all)
other
(sig append
  ((listof :a) (listof :a))
  =>
  (listof :a))
other
(sig append
  ((alistof :a :b) (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig app
  ((listof :a) (listof :a))
  =>
  (listof :a))
other
(sig app
  ((alistof :a :b) (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig rev
  ((listof :a))
  =>
  (listof :a))
other
(sig rev
  ((alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig nth
  (nat (listof :a))
  =>
  :a :satisfies (< x1 (len x2)))
other
(sig cons
  (:a (listof :a))
  =>
  (listof :a))
other
(sig fix-true-list
  ((listof :a))
  =>
  (listof :a))
other
(sig fix-true-list
  ((alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig last
  ((listof :a))
  =>
  (listof :a))
other
(sig last
  ((alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig repeat
  (nat :a)
  =>
  (listof :a))
other
(sig make-list-ac
  (nat :a (listof :a))
  =>
  (listof :a))
other
(sig nthcdr
  (nat (listof :a))
  =>
  (listof :a))
other
(sig nthcdr
  (nat (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig remove
  (all (listof :a))
  =>
  (listof :a))
other
(sig remove
  (all (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig remove1-equal
  (all (listof :a))
  =>
  (listof :a))
other
(sig remove1-equal
  (all (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig remove-duplicates
  ((listof :a))
  =>
  (listof :a))
other
(sig remove-duplicates
  ((alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig cdr
  ((listof :a))
  =>
  (listof :a))
other
(sig cdr
  ((alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig revappend
  ((listof :a) (listof :a))
  =>
  (listof :a))
other
(sig revappend
  ((alistof :a :b) (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig reverse
  ((listof :a))
  =>
  (listof :a))
other
(sig reverse
  ((alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig set-difference$
  ((listof :a) (listof :a))
  =>
  (listof :a))
other
(sig set-difference$
  ((alistof :a :b) (alistof :a :b))
  =>
  (alistof :a :b)
  :suffix alistof)
other
(sig first-n-ac
  (nat (listof :a) (listof :a))
  =>
  (listof :a)
  :satisfies (< x1 (len x2)))
other
(sig first-n-ac
  (nat (alistof :a :b) (alistof :a :b))
  =>
  (alistof :a :b)
  :satisfies (< x1 (len x2))
  :suffix alistof)
other
(local (in-theory (enable take)))
other
(sig take
  (nat (listof :a))
  =>
  (listof :a)
  :satisfies (<= x1 (len x2))
  :hints (("Goal" :cases ((equal x1 (len x2))))))
other
(sig take
  (nat (alistof :a :b))
  =>
  (alistof :a :b)
  :satisfies (<= x1 (len x2))
  :suffix alistof
  :hints (("Goal" :cases ((equal x1 (len x2))))))
other
(local (in-theory (e/d (natp) (take))))
other
(sig subseq-list
  ((listof :a) nat nat)
  =>
  (listof :a)
  :satisfies (and (<= x3 (len x1))
    (<= x2 x3)))
other
(sig subseq-list
  ((alistof :a :b) nat nat)
  =>
  (alistof :a :b)
  :satisfies (and (<= x3 (len x1))
    (<= x2 x3))
  :suffix alistof)
other
(sig subseq
  ((listof :a) nat nat)
  =>
  (listof :a)
  :satisfies (and (<= x3 (len x1))
    (<= x2 x3)))
other
(sig subseq
  ((alistof :a :b) nat nat)
  =>
  (alistof :a :b)
  :satisfies (and (<= x3 (len x1))
    (<= x2 x3))
  :suffix alistof)
other
(sig put-assoc-equal
  (:a :b (alistof :a :b))
  =>
  (alistof :a :b))
other
(sig pairlis$
  ((listof :a) (listof :b))
  =>
  (alistof :a :b)
  :satisfies (= (len x1) (len x2)))
other
(sig update-nth
  (nat :a (listof :a))
  =>
  (listof :a)
  :satisfies (<= x1 (len x3)))
other
(sig remove-dups-aux
  ((listof :a) (listof :a))
  =>
  (listof :a))
other
(sig remove-dups
  ((listof :a))
  =>
  (listof :a))