with-supporters-test-sub

other

(in-package "ACL2")

mac1-fnfunction

(defun mac1-fn (x) x)

mac1macro

(defmacro mac1 (x) (mac1-fn x))

g1function

(defun g1 (x) (declare (xargs :guard t)) (mac1 x))

mac2-fn-bfunction

(defun mac2-fn-b (x) x)

mac2-fnfunction

(defun mac2-fn (x) (mac2-fn-b x))

mac2macro

(defmacro mac2 (x) (mac2-fn x))

other

(add-macro-alias mac2 g2)

g2function

(defun g2
  (x)
  (declare (xargs :guard (g1 x)
      :guard-debug t
      :guard-hints (("Goal" :do-not '(preprocess)))))
  (mac2 x))

g3function

(defun g3 (x) (g2 x))

g4function

(defund g4 (x) (declare (xargs :guard t)) (consp x))

g5function

(defun g5 (x) (declare (xargs :guard (g4 x))) (car x))

other

(defstobj st fld)

other

(defstub stub1 (x) t)

g6function

(defun g6 (x) (declare (xargs :guard t)) x)

other

(defattach stub1 g6)

other

(defstub stub2 (x) t)

g7function

(defun g7 (x) (declare (xargs :guard t)) (cons x x))

g8function

(defun g8 (x) (declare (xargs :guard t)) (list x x))

other

(defattach (stub1 g7) (stub2 g8))

other

(defstub stub3 (x) t)

g9function

(defund g9 (x) (declare (xargs :guard t)) (len x))

other

(defattach stub3 g9)

g10function

(defun g10 (x) x)

other

(verify-guards g10)

g11function

(defun g11 (x) (declare (xargs :guard t)) (g10 x))

g12function

(defun g12 (x) (declare (xargs :mode :program)) x)

other

(verify-termination g12)

g13function

(defun g13 (x) (g12 x))

g-progencapsulate

(encapsulate nil (program) (defun g-prog (x) x))

macmacro

(defmacro mac (x) (g-prog x))

other

(table my-tbl nil nil :guard (g13 val))

other

(table my-tbl 3 4)

other

(table my-tbl 3 5)

g14function

(defun g14 (x) x)

e1-propencapsulate

(encapsulate ((e1 (x) t))
  (local (defun e1 (x) x))
  (defthm e1-prop (equal (g14 (e1 x)) x)))

g15function

(defun g15 (x y) (< x y))

g16function

(defun-sk g16 (x) (exists y (g15 x y)))

g17function

(defun g17 (x) (cons x x))

*c*constant

(defconst *c* (g17 3))

g18function

(defun g18 (x) (cons *c* x))