• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Oslib
      • Std/io
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • Startup-banner
      • Command-line
        • Save-exec
        • Argv
        • Getopt
          • Demo-p
          • Defoptions
          • Demo2
          • Parsers
          • Sanity-check-formals
          • Formal->parser
          • Formal->argname
            • Formal->longname
            • Formal->merge
            • Formal->alias
            • Formal->usage
            • Formal->hiddenp
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Getopt

    Formal->argname

    Signature
    (formal->argname x world) → argname
    Arguments
    x — Guard (formal-p x).
    world — Guard (plist-worldp world).
    Returns
    argname — Type (stringp argname).

    Definitions and Theorems

    Function: formal->argname

    (defun
        formal->argname (x world)
        (declare (xargs :guard (and (formal-p x)
                                    (plist-worldp world))))
        (let ((__function__ 'formal->argname))
             (declare (ignorable __function__))
             (b* (((formal x) x)
                  (custom (assoc :argname x.opts))
                  ((when (stringp (cdr custom)))
                   (cdr custom))
                  ((when custom)
                   (raise "In ~x0, :argname is not even a stringp: ~x1."
                          x.name (cdr custom)))
                  (parser (formal->parser x world))
                  ((when (equal parser 'parse-plain)) ""))
                 "ARG")))