FORALL

Major Section:  DEFUN-SK

The symbol forall (in the ACL2 package) represents universal quantification in the context of a defun-sk form. See defun-sk and see exists.

See quantifiers for an example illustrating how the use of recursion, rather than explicit quantification with defun-sk, may be preferable.