Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 19-Aug-2021 13:48:53 JST きゅーけー

   ACL2、program モードで関数を定義すれば何も証明してくれない代わりに副作用使い放題なことがわかった。これで ACL2 でスクリプトをバリバリ書いていけるぞ。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 19-Aug-2021 13:49:31 JST きゅーけー

     in reply to

     どこまで program モードの範囲を限定できるかが肝だ。