Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 31-Dec-2021 03:50:26 JST きゅーけー

   ACL2 の学習行動が消去されつつあるんで、ちょっと Coalton の方にいってもいい気がする。ACL2 の学習、なんか修行みたいで辛すぎるんだもん。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 31-Dec-2021 03:51:20 JST きゅーけー

     in reply to

     ACL2 で無限集合が扱えないので ACL2 を使って集合論をやって遊ぶということができなかったのも大きい。。。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 31-Dec-2021 03:52:09 JST きゅーけー

     in reply to

     しかし、せっかく整列集合と超限順序数のことが分かるようになってきたのに ACL2 をやらないのは勿体ない気がするな。