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 >
