ACL2 で書いたブラックジャック、任意の枚数のカードで、score が 11 以下のときにもう一回カードを引いても BUST しない定理の証明に成功したのでだいたい満足した。 https://gitlab.com/tojoqk/blackjack/-/commit/60143c0e574d00a1571bd0750ca7186cdc4d04dc
Conversation
Notices
-
きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 24-Jan-2021 03:31:36 JST きゅーけー -
きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 24-Jan-2021 03:35:18 JST きゅーけー シャワーを浴びているときに、ace のスコア計算で無駄に再帰しているせいで証明が大変になっていることに気づいた。https://gitlab.com/tojoqk/blackjack/-/commit/4bf52294c02c89c5cbd44689fcf573bb29cf1204
In conversation permalink
-