• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
          • Math-lemmas
          • Ihs-theories
          • Ihs-init
            • Ihs-utilities
              • Defun-type/exec-theory
              • Defun-theory
              • Definition-free-theory
              • Rewrite-theory
              • Rewrite-free-theory
              • Definition-theory
              • Mlambda
                • Enable-theory
                • Disable-theory
            • Logops
          • Rtl
        • Algebra
      • Testing-utilities
    • Ihs-utilities

    Mlambda

    Macro LAMBDA form.

    Example:

    (DEFMACRO X/Y-GUARD (X Y)
      (MLAMBDA (X Y) (AND (RATIONALP X) (RATIONALP Y) (NOT (EQUAL Y 0)))))
    
      =
    
    (DEFMACRO X/Y-GUARD (X Y)
      (LIST 'AND (LIST 'RATIONALP X) (LIST 'RATIONALP Y)
            (LIST (LIST 'NOT (LIST 'EQUAL Y 0)))))
    
    =
    
    (DEFMACRO X/Y-GUARD (X Y)
      `(AND (RATIONALP ,X) (RATIONALP ,Y) (NOT (EQUAL ,Y 0))))

    MLAMBDA is a macro LAMBDA. MLAMBDA converts form to a lisp macro body, substituting all symbols except those that appear in the args with the quoted symbol.