Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 06-Aug-2021 01:20:26 JST きゅーけー

   ACL2 が証明に失敗したときに、適切なヒントを出せるようになってきたな。最初の頃と比較してヒントを考える時間が明らかに短くなっている。まあ、今やっているのが簡単な問題だからというだけかもしれんけど。code: https://git.tojo.tokyo/acl2-theorems.git/commit/?id=80ff85f0f558e31a5aff784b2d38547c870f9d95CI: https://ci.tojo.tokyo/jobs/acl2-verify/169

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 06-Aug-2021 01:24:03 JST きゅーけー

     in reply to

     と思って ACL2 の出力を眺めていたら無駄なヒントを出していたことに気づいて消した。ACL2 マスターまでの道は長い。https://git.tojo.tokyo/acl2-theorems.git/commit/?id=12132a24ad279fd3c1443cb79d52f897acaa49a7