Parallel evaluation of arguments in a function call
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism, and see parallel-programming, which has a disclaimer.
Example Forms: (pargs (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2)))) (pargs (declare (granularity (> x 35))) (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2)))) General Form: (pargs (declare (granularity expr)) ; optional granularity declaration (f arg1 ... argN))
Since macros can change expressions in unexpected ways, it is illegal to
See parallelism-at-the-top-level for restrictions on evaluating parallelism primitives from within the ACL2 top-level loop.