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 (using ACL2 Version 3.0,
built on Allegro Common Lisp).
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)
NIL
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 wet for how you might be able to get an error backtrace.
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 wet for how you might be able to get an error backtrace.
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. 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)
NIL
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. 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
Goal
(IMPLIES (POSP X)
(O< (ACL2-COUNT (+ -1 X))
(ACL2-COUNT X))).
By the simple :definition POSP we reduce the conjecture to
Goal'
(IMPLIES (AND (INTEGERP X) (< 0 X))
(O< (ACL2-COUNT (+ -1 X))
(ACL2-COUNT X))).
But we reduce the conjecture to T, by case analysis.
Q.E.D.
That completes the proof of the measure theorem for FACT. Thus, we
admit this function under the principle of definition. We observe that
the type of FACT is described by the theorem
(AND (INTEGERP (FACT X)) (< 0 (FACT X))). We used the :compound-recognizer
rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.
Summary
Form: ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
(:DEFINITION NOT)
(:DEFINITION POSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FACT
ACL2 >(trace$ fact)
NIL
ACL2 >:set-guard-checking t
Turning guard checking on, value T.
ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::FACT 2)
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited
on recursive calls of the executable counterpart (i.e., in the ACL2
logic) of FACT. To check guards on all recursive calls:
(set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
(set-guard-checking :nowarn)
<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 wet for how you might be able to get an error backtrace.
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 wet for how you might be able to get an error backtrace.
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)
<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. To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-
checking.
ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::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 >(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.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FACT
ACL2 >(trace$ fact)
NIL
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 wet for how you might be able to get an error backtrace.
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 wet for how you might be able to get an error backtrace.
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)
<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. 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
Goal
(IMPLIES (POSP X)
(O< (ACL2-COUNT (+ -1 X))
(ACL2-COUNT X))).
By the simple :definition POSP we reduce the conjecture to
Goal'
(IMPLIES (AND (INTEGERP X) (< 0 X))
(O< (ACL2-COUNT (+ -1 X))
(ACL2-COUNT X))).
But we reduce the conjecture to T, by case analysis.
Q.E.D.
That completes the proof of the measure theorem for FACT. Thus, we
admit this function under the principle of definition. We observe that
the type of FACT is described by the theorem
(AND (INTEGERP (FACT X)) (< 0 (FACT X))). We used the :compound-recognizer
rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.
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: ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
(:DEFINITION NOT)
(:DEFINITION POSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION FACT))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FACT
ACL2 >(trace$ fact)
NIL
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 wet for how you might be able to get an error backtrace.
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 wet for how you might be able to get an error backtrace.
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)
<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. 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
Goal
(IMPLIES (POSP X)
(O< (ACL2-COUNT (+ -1 X))
(ACL2-COUNT X))).
By the simple :definition POSP we reduce the conjecture to
Goal'
(IMPLIES (AND (INTEGERP X) (< 0 X))
(O< (ACL2-COUNT (+ -1 X))
(ACL2-COUNT X))).
But we reduce the conjecture to T, by case analysis.
Q.E.D.
That completes the proof of the measure theorem for FACT. Thus, we
admit this function under the principle of definition. We observe that
the type of FACT is described by the theorem
(AND (INTEGERP (FACT X)) (< 0 (FACT X))). We used the :compound-recognizer
rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.
Summary
Form: ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
(:DEFINITION NOT)
(:DEFINITION POSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FACT
ACL2 >(trace$ fact)
NIL
ACL2 >:set-guard-checking t
Turning guard checking on, value T.
ACL2 !>(fact 2)
1> (ACL2_*1*_ACL2::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 !>: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)
<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. To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-
checking.
ACL2 >(fact 2)
1> (ACL2_*1*_ACL2::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 >(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
ACL2 >(trace$ fact)
NIL
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. 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 >
