definline - ACL2 Book

other

(in-package "ACL2")

definlinemacro

(defmacro definline
  (name formals &rest args)
  `(defun-inline ,NAME ,FORMALS . ,ARGS))

definlinedmacro

(defmacro definlined
  (name formals &rest args)
  `(defund-inline ,NAME ,FORMALS . ,ARGS))

local

(local (progn (defun test (x) (declare (xargs :guard (natp x))) (+ 1 x))
    (definline test2
      (x)
      (declare (xargs :guard (natp x)))
      (+ 1 x))
    (defun f (x) (test x))
    (defun g (x) (test2 x))))