These terms control options for the logic of the ACL2 theorem prover.
If passed t, functions will be compiled as you go along.
If passed t, unused formals and locals will be allowed without an ignore or ignorable declaration.
If passed t, irrelevant formals will be allowed in definitions.
If passed t, STATE will be allowed as a formal parameter.