• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Community
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • 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
      • 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.