(make-event
 '(defun test1 (x)
    (cons x x)))

(make-event
 (value '(defun test2 (x)
	   x))
 :check-expansion t)

(make-event
 (value '(defun test3 (x)
	   x))
 :check-expansion (defun test3 (x)
                    x))

(encapsulate
 ((foo (x) t))
 (local (make-event '(defun foo (x) (cons x x))))
 (defthm foo-prop
   (consp (foo x))))

(encapsulate
 ((foo2 (x) t))
 (local (make-event '(defun foo2 (x) (cons x x))
                    :check-expansion t))
 (defthm foo2-prop
   (consp (foo2 x))))

(encapsulate
 ((foo3 (x) t))
 (local (make-event '(defun foo3 (x) (cons x x))
                    :check-expansion
                    (defun foo3 (x) (cons x x))))
 (defthm foo3-prop
   (consp (foo3 x))))

(encapsulate
 ()
 (make-event '(defun bar (x) (cons x x)))
 (defthm bar-prop
   (consp (bar x))))

(encapsulate
 ()
 (make-event '(defun bar2 (x) (cons x x))
             :check-expansion t)
 (defthm bar2-prop
   (consp (bar2 x))))

(encapsulate
 ()
 (make-event '(defun bar3 (x) (cons x x))
             :check-expansion
             (defun bar3 (x) (cons x x)))
 (defthm bar3-prop
   (consp (bar3 x))))

(encapsulate
 ((local-fn (x) t))
 (local (defun local-fn (x) x))
 (make-event '(defun bar4 (x) (cons x x))
             :check-expansion nil)
 (defthm bar4-prop
   (consp (bar4 x))))

(certify-book "portcullis-expansion" ?)