Major Section: EVENTS
Examples: ACL2 !>(defstub subr1 (* * state) => (mv * state)) ACL2 !>(defstub add-hash (* * hash-table) => hash-table)General Forms: (defstub name args-sig => output-sig) (defstub name args-sig => output-sig :doc doc-string)
Name is a new function symbol and (name . args-sig) => output-sig)
is a signature. If the optional doc-string is supplied
it should be a documentation string. See also the ``Old Style''
heading below.
Defstub macro expands into an encapsulate event
(see encapsulate). Thus, no axioms are available about name
but it may be used wherever a function of the given signature is
permitted.
Old Style:
Old Style General Form: (defstub name formals output) (defstub name formals output :doc doc-string)where
name is a new function symbol, formals is its list of
formal parameters, and output is either a symbol (indicating
that the function returns one result) or a term of the form
(mv s1 ... sn), where each si is a symbol (indicating that the
function returns n results). Whether and where the symbol
state occurs in formals and output indicates how the
function handles state. It should be the case that
(name formals output) is in fact a signature (see signature).
Note that with the old style notation it is impossible to stub-out
a function that uses any single-threaded object other than state.
The old style is preserved for compatibility with earlier versions of
ACL2.