• 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
            • Custom-parser
            • Parse-nat
            • Parse-plain
            • Parse-string
            • Parse-pos
            • Defparser
            • Sanity-check-formals
            • Formal->parser
            • Formal->argname
            • Formal->longname
            • Formal->alias
            • Formal->usage
            • Formal->merge
            • Formal->hiddenp
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Parsers

    Defparser

    Register a new argument-parsing function with getopt.

    (defparser fn &key predicate) is a macro for registering parsing functions with getopt.

    It first checks to make sure that fn has the valid format for a custom-parser, and tries to prove the necessary progress property.

    If predicate is non-nil, it installs fn as the default parsing function to use for options of type predicate. The general idea here is that if you write a new custom parser for ports, you can then set it up to be the default parser for any port-p field.