Defstub
Stub-out a function symbol
Examples:
ACL2 !>(defstub subr1 (* * state) => (mv * state))
ACL2 !>(defstub add-hash (* * hashtable) => hashtable)
ACL2 !>(defstub inv (*) => * :formals (x) :guard (fieldp x))
General Forms:
(defstub name (i1 ... ik) => outputs :kwd1 val1 ... :kwdn valn) ; new style
(defstub name (i1 ... ik) outputs :kwd1 val1 ... :kwdn valn) ; old style
where name is a new function symbol, and (i1 ... ik),
outputs, :kwdi, and vali must be as follows, respectively.
- New style: ((name i1 ... ik) => outputs :kwd1 val1 ... :kwdn
valn) is a valid new-style signature.
- Old style: (name (i1 ... ik) outputs :kwd1 val1 ... :kwdn
valn) is a valid old-style signature.
Also see signature. Note that (i1 ... ik) is the
list of formal parameters of the newly-defined function symbol, name.
Note that while the defstub syntax resembles a signature, it is
different: name occurs outside the parentheses containing (i1
... ik) in the defstub syntax, but inside in the signature syntax.
A defstub macro call 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 outputs is of the form (mv ...), then a :type-prescription rule is introduced stating that name returns a value
satisfying true-listp.
