model-macros.lisp « rtl « support « kaufmann « 2003 « workshops « books - acl2 - Debian dgit repo for package acl2

summary refs log tree commit diff

path: root/books/workshops/2003/kaufmann/support/rtl/model-macros.lisp

blob: 8e19a6e7ad36443d78fc32e07321ff17dcd885a9 (plain)

(in-package "ACL2")

(defmacro out1 (n)
          (list 'out1$ n '$path))

(defmacro out2 (n)
          (list 'out2$ n '$path))