Major Section: ACL2-BUILT-INS

Implies is the ACL2 implication function. (implies P Q) means that either P is false (i.e., nil) or Q is true (i.e., not nil).

Implies

(implies P Q)

P

nil

Q

To see the ACL2 definition of this function, see pf.