From d3b19b77771812f12420e378857dead647728745 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 22 Jan 2021 23:42:56 +0900 Subject: Remove hints. --- blackjack.lisp | 10 +++------- 1 file 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))) - -- cgit v1.2.3