DEFSTUB

stub-out a function symbol
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. Exception: if output-sig is of the form (mv ...), then a :type-prescription rule is introduced stating that name returns a value satisfyig true-listp.

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.