Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 21:27:17 JST きゅーけー

   なんか Coq で集合論できそうな気配がするので Coq と Proof General のインストールを始めた。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 21:28:24 JST きゅーけー

     in reply to

     ACL2 を使っていきたかったが、無限の誘惑には勝てなかった……。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 21:32:28 JST きゅーけー

     in reply to

     無限集合に飽きたら ACL2 に戻ろう。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 21:57:18 JST きゅーけー

     in reply to

     コンビニによって帰ってきたら、冷静に考えてみたら別に数学をすることではなくてプログラムの性質を証明したいのであって順序数についてある程度分かったなら ACL2 をやったらよくね？って気が変わって ACL2 モチベが上がってきた。これぞ諸行無常……。