• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
      • Make-event
      • Defmacro
      • Untranslate-patterns
      • Tc
      • Macro-aliases-table
      • Macro-args
        • Set-duplicate-keys-action
      • Defabbrev
      • User-defined-functions-table
      • Untranslate-for-execution
      • Trans
      • Add-macro-fn
      • Check-vars-not-free
      • Safe-mode
      • Macro-libraries
      • Defmacro-untouchable
      • Trans1
      • Set-duplicate-keys-action
      • Add-macro-alias
      • Magic-macroexpand
      • Defmacroq
      • Remove-macro-fn
      • Remove-macro-alias
      • Add-binop
      • Untrans-table
      • Trans!
      • Remove-binop
      • Tcp
      • Tca
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Macro-args
• Macros
• Programming
• Advanced-features

Set-duplicate-keys-action

Control action for macro calls with duplicate keyword arguments

Example Forms:
(set-duplicate-keys-action thm :warning)
(set-duplicate-keys-action my-macro-1 nil)

General Forms:
(set-duplicate-keys-action name :error)
(set-duplicate-keys-action name :warning)
(set-duplicate-keys-action name nil)

where name is a symbol, one that is generally expected to be the name of a macro.

By default, an error occurs when ACL2 encounters a macro call with duplicate keys, for example (foo 3 :y 4 :y 5) where :y is a keyword argument of the macro, foo. However, the event (set-duplicate-keys-action name val) can be used to determine whether such duplicate keys cause an error, a warning, or neither, according to whether val is the keyword :error, :warning, or nil, respectively.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. It is local to the book or encapsulate form in which it occurs; see set-duplicate-keys-action! for a corresponding non-local event. Indeed, (set-duplicate-keys-action ...) is equivalent to (local (set-duplicate-keys-action! ...)).