		Search-engine friendly clone of the ACL2 documentation.

Pattern-match

Pattern-match-list

Pattern matching to a list of terms.

Example:

(pattern-match-list
  (a b c d)
  (((cons !c x) 3 (list* !b y) x)
   (declare (ignore x))
   (foo y))
  (& default-value)))

pml is a convenient abbreviaton of pattern-match-list.

Matches a list of terms to a list of pattern clauses. See pattern-match for more documentation of the pattern semantics. The first argument to pattern-match-list should be a list of input terms. (For best efficiency, these terms should be bound variables or simple constants, not containing function calls.) Each subsequent argument should be a pattern clause, consisting of a list of the following items:

a list of patterns, the same length as the list of input terms
a declare form, used when evaluating the test forms (optional)
any number of test forms, which may use variables bound in the pattern (optional)
a declare form whose scope is the body (optional)
the body, an expression to be evaluated if the pattern matches and all the tests succeed.

The final pattern clause may be of the form (& default-value); this is an exception to the convention that the pattern list must be a list same length as the input list, and it simply defines a default value for the pattern-match clause, to be returned instead of nil when all patterns fail.

See also pattern-matches-list, which simply tests whether or not a certain pattern list matches the list of inputs.