GUARD-EVALUATION-EXAMPLES-LOG

log showing combinations of defun-modes and guard-checking
Major Section:  GUARD

See guard-evaluation-examples-script for a script that shows the interaction of defun-modes with the value set by set-guard-checking. Here, we present a log resulting from running this script.

See set-guard-checking for discussion of the interaction between defun-modes and guard-checking that is illustrated by this script. Also see guard-evaluation-table for a succinct table, with associated discussion, that covers in detail the interactions illustrated here.

ACL2 !>(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :mode :program))
         (if (posp x)
             (* x (fact (1- x)))
           1))

Summary
Form:  ( DEFUN FACT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 !>(trace$ fact)
 ((FACT))
ACL2 !>:set-guard-checking t

Guard-checking-on already has value T.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
FACT, which is (INTEGERP X), is violated by the arguments in the call
(FACT T).  See :DOC trace for a useful debugging utility.  See :DOC
set-guard-checking for information about suppressing this check with
(set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
FACT, which is (INTEGERP X), is violated by the arguments in the call
(FACT T).  See :DOC trace for a useful debugging utility.  See :DOC
set-guard-checking for information about suppressing this check with
(set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:u

          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 >(defun fact (x)
         (declare (xargs :guard t
                         :mode :program))
         (if (posp x)
             (* x (fact (1- x)))
           1))

Summary
Form:  ( DEFUN FACT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 >(trace$ fact)
 ((FACT))
ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:u

          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 >(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :verify-guards nil
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))

For the admission of FACT we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is

[[output omitted here]]

Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 >(trace$ fact)
 ((FACT))
ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2)
[[Comment added to the log:
  Normally you would get a message about guard-checking being
  inhibited on recursive calls.  However, when a function is
  traced the guard-checking is done on recursive calls unless
  the guards have been verified (see :DOC verify-guards).
]]
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC trace for a useful debugging utility.  See :DOC set-guard-
checking for information about suppressing this check with (set-guard-
checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC trace for a useful debugging utility.  See :DOC set-guard-
checking for information about suppressing this check with (set-guard-
checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
[[Comment added to the log:
  In spite of the warning above, guards are checked here on
  self-recursive calls, because the function is traced.
]]
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >(verify-guards fact)

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound-
recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
and the :type-prescription rule FACT.  FACT is compliant with Common
Lisp.

Summary
Form:  ( VERIFY-GUARDS FACT)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FACT))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 FACT
ACL2 >(trace$ fact)
 ((FACT))
ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC trace for a useful debugging utility.  See :DOC set-guard-
checking for information about suppressing this check with (set-guard-
checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC trace for a useful debugging utility.  See :DOC set-guard-
checking for information about suppressing this check with (set-guard-
checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:u
 L        1:x(DEFUN FACT (X) ...)
ACL2 >:u
          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 >(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))

For the admission of FACT we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is

[[output omitted here]]

Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 >(trace$ fact)
 ((FACT))
ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC trace for a useful debugging utility.  See :DOC set-guard-
checking for information about suppressing this check with (set-guard-
checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC trace for a useful debugging utility.  See :DOC set-guard-
checking for information about suppressing this check with (set-guard-
checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:u
          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 >(defun fact (x)
         (declare (xargs :guard t
                         :verify-guards nil
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))

For the admission of FACT we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is

[[output omitted here]]

Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 >(trace$ fact)
 ((FACT))
ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (ACL2_*1*_ACL2::FACT 1)
    3> (ACL2_*1*_ACL2::FACT 0)
    <3 (ACL2_*1*_ACL2::FACT 1)
  <2 (ACL2_*1*_ACL2::FACT 1)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >(verify-guards fact)

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound-
recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription
rule FACT.  FACT is compliant with Common Lisp.

Summary
Form:  ( VERIFY-GUARDS FACT)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:TYPE-PRESCRIPTION FACT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT

[[Note added to log: No need to trace fact again after verify-guards.]]

ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !>(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !>:set-guard-checking :none

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
  2> (FACT 2)
    3> (FACT 1)
      4> (FACT 0)
      <4 (FACT 1)
    <3 (FACT 1)
  <2 (FACT 2)
<1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 >(fact t)
1> (ACL2_*1*_ACL2::FACT T)
  2> (FACT T)
  <2 (FACT 1)
<1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 >