diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-22 23:42:56 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-22 23:42:56 +0900 |
| commit | d3b19b77771812f12420e378857dead647728745 (patch) | |
| tree | 44b1e87867adfca16f6b9ff60677d9c25041c966 | |
| parent | 20c2ddae29df77e9b5cf60c07f3b85b3609f75bd (diff) | |
Remove hints.
| -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))) - |