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

    Formal->hiddenp

    Signature
    (formal->hiddenp x) → longname
    Arguments
    x — Guard (formal-p x).
    Returns
    longname — Type (stringp longname).

    Definitions and Theorems

    Function: formal->hiddenp

    (defun formal->hiddenp (x)
      (declare (xargs :guard (formal-p x)))
      (let ((__function__ 'formal->hiddenp))
        (declare (ignorable __function__))
        (b* (((formal x) x)
             (hide (cdr (assoc :hide x.opts)))
             ((when hide) t))
          nil)))