Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:53:41 JST きゅーけー

   う、ACL2 の arithmetic ライブラリをロードしようと思って調べたら雑な自分の記事がでてきてつらい……。Japan を有効にしてなければ出てこないだけ幸いである。

   これ> 証明に成功しました。定理ライブラリの力は凄いですね。とか書いてあるやつなので検索されて見つけられるの恥かしいんだよな。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:56:37 JST きゅーけー

     in reply to

     というか、なんでタイトル ACL2 じゃなくて Acl2 になってるんだろう。即座に直そう……。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 02-Jan-2022 15:58:28 JST きゅーけー

     in reply to

     あれ？ちゃんと全部大文字だった。どこで ACL2 が Acl2 に変わったんだろう。