• Top
    • Documentation
      • Xdoc
      • ACL2-doc
      • Pointers
      • Doc
      • Documentation-copyright
      • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
      • Books
      • Recursion-and-induction
      • Boolean-reasoning
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Documentation

    Args

    args, guard, type, constraint, etc., of a function symbol

    Example:
    :args assoc-eq

    Args takes one argument, a symbol which must be the name of a function or macro, and prints out some information about it including the formal parameters, the guard expression, the output signature, the deduced type, the constraint (if any), and its badge and warrant, if any.