diff options
| -rw-r--r-- | blackjack.lisp | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/blackjack.lisp b/blackjack.lisp index 4e197f4..1cee403 100644 --- a/blackjack.lisp +++ b/blackjack.lisp @@ -114,8 +114,7 @@ (natp (score* rl)))) (defun score (rl) - (declare (xargs :guard (rank-list-p rl) - :guard-hints (("Goal" :use natp/score*)))) + (declare (xargs :guard (rank-list-p rl))) (let ((s (score* rl))) (cond ((and (< 21 s)) 'BUST) @@ -130,8 +129,7 @@ (defthm scorep/score (implies (rank-list-p x) - (scorep (score x))) - :hints (("Goal" :use scorep/score-1))) + (scorep (score x)))) (defun judge/score (player dealer) (declare (xargs :guard (and (scorep player) @@ -150,8 +148,7 @@ (defun judge/ranks (player dealer) (declare (xargs :guard (and (rank-list-p player) - (rank-list-p dealer)) - :guard-hints (("Goal" :use scorep/score)))) + (rank-list-p dealer)))) (judge/score (score player) (score dealer))) @@ -162,4 +159,3 @@ (implies (facep r) (equal (score (list 'A r)) 'NATURAL-BLACKJACK))) - |