https://twitter.com/kinaba のログ (twilog の方が便利です。)
| あ、そうか、induction n で解けてしまうのか。もっとcofixcofixした問題を考えよう #anapr | |
| @lyrical_logical set::count() と set::find() の話では。 | |
| @mr_konn 多分あなぷるの Peirce のことかと勝手に推測したのですけど、Classical.Periceを用いてカレントのPeirceを証明してるのでセーフです＞証明対象の命題自体を用いて証明。ハイチュウ率から出すバージョンも投稿してみた | |
| ナナカ http://take-hisa.com/nanaka/ さん、ダンジョン１つクリアする度に２つずつダンジョン増えるんですけど、この無限性を余帰納的に表現すると問題１つ作れませんかね。 | |
| @kikx おおなるほど。replace も ring も数時間前まで使ったことがなかったという… | |
| @mr_konn 古典でしか成立しない定理を使わないと解けない（＆どれでもいいから１個１回使えば解ける）のは知っていたので、Classical_Propモジュールを「ど・れ・に・し・よ・う・か・な」と眺めてたらPeirce則の特殊版がそのままあったので使ってみた、という流れでした | |
| @mr_konn 論理結合子だけしか使ってないようなプリミティブな定理だと、この辺は言語組み込みの構文みたいなものなので逆にSearchとか使いどころがないですけど、自然数の公理系やなんかを使う証明だと、SearchPattern コマンドで合う定理を探すのは結構やります。 |