• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
        • 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
    • Macros

    Trans1

    Print the one-step macroexpansion of a form

    See term for background on translated and untranslated terms, including some discussion of macros.

    Examples:
    :trans1 (list a b c)
    :trans1 (caddr x)
    :trans1 (cond (p q) (r))

    This utility takes one argument, an alleged untranslated term, and expands the top-level macro in it for one step only. Either an error is caused, which happens when the form is not a call of a macro, or the result is printed. Also see trans, which translates the given form completely.

    On very rare occasions, complete translation is not quite the same as translating the output of :trans1, though the two should still be logically equivalent. This can happen for a call of stobj-let in the body of a function: its translation may include a check for duplicate indices that is omitted in the single-step macroexpansion.