• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
        • Fast-alists
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Efficiency
        • Irrelevant-formals
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
        • Set-register-invariant-risk
        • Strings
        • Program-wrapper
        • Get-internal-time
        • Basics
          • Let
          • Return-last
          • Mv-let
          • Flet
          • Or
          • Mv
          • And
            • Booleanp
            • If
            • Not
            • Equal
            • Implies
            • Iff
            • Macrolet
            • Quote
            • Let*
            • Case-match
            • ACL2-count
            • Case
            • Good-bye
            • Cond
            • Null
            • Progn$
            • Identity
            • Xor
          • Packages
          • Oracle-eval
          • Defmacro-untouchable
          • <<
          • Primitive
          • Revert-world
          • Unmemoize
          • Set-duplicate-keys-action
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Fake-oracle-eval
          • Defopen
          • Sleep
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Basics
    • ACL2-built-ins

    And

    Conjunction

    And is the macro for conjunctions. And takes any number of arguments. And returns nil if one of the arguments is nil, but otherwise returns the last argument. If there are no arguments, and returns t.

    And is a Common Lisp macro. See any Common Lisp documentation for more information.

    Macro: and

    (defmacro and (&rest args)
      (and-macro args))

    Function: and-macro

    (defun and-macro (lst)
      (declare (xargs :guard t))
      (if (consp lst)
          (if (consp (cdr lst))
              (list 'if
                    (car lst)
                    (and-macro (cdr lst))
                    nil)
            (car lst))
        t))