Support
Miscellaneous supporting functions used by the std/util library.
Subtopics
- Extract-keywords
- Extract legal keyword/value pairs from an argument list.
- Dumb-string-sublis
- Non-recursively applies a list of substring substitutions to a string.
- Raise
- Shorthand for causing hard errors.
- Look-up-return-vals
- (look-up-return-vals fn world) returns the stobjs-out property for
fn. This is a list that may contain nils and ACL2::stobj names,
with the same length as the number of return vals for fn.
- Logic-mode-p
- (logic-mode-p fn world) looks up the function fn and returns
t if fn is in logic mode, or nil otherwise. It causes a
hard error if fn isn't a function.
- Look-up-wrapper-args
- (look-up-wrapper-args wrapper world) is like look-up-formals, except
that wrapper can be either a function or a macro, and in the macro case
the arguments we return may include lambda-list keywords; see macro-args.
- Look-up-formals
- (look-up-formals fn world) looks up the names of the arguments of the
function fn, or causes a hard error if fn isn't a function.
- Legal-kwds-p
- List of legal keywords for extract-keywords.
- Split-///
- Split an argument list into pre- and post-/// contents.
- Keyword-legality
- Check whether x is a legal keyword
- Getarg+
- Get a value from the keyword-value alist produced by extract-keywords, with default-value support, and additionally return a flag
saying whether the key was bound. Returns (mv value boundp).
- Var-is-stobj-p
- (var-is-stobj-p var world) checks whether var is currently the name
of a ACL2::stobj.
- Look-up-guard
- (look-up-guard fn world) looks up the guard of the function fn, or
causes a hard error if fn isn't a function.
- Getarg
- Get a value from the keyword-value alist produced by extract-keywords, with default-value support.
- Cons-listp
- (cons-listp x) is like alistp but does not require the
list to be nil-terminated.
- Tuplep
- (tuplep n x) recognizes nil-terminated n-tuples.
- Tuple-listp
- (tuple-listp n x) recognizes a list of nil-terminated n-tuples.
- Ends-with-period-p
- Determines if a string ends with a period.
