24/04/19 12:06:54.47 0YEF9E1Q.net
まず代数計算は自動化したいよね
ほぼ定義を再掲するだけみたいな証明は自動で演繹できるようにしたい
全部が全部そうできなくてもいいけど、書き方に若干のルールを設ければ自動で証明できる範囲は広がるはず
型駆動でも、OOPでいうとこのデザインパターンを発見して、
>>10や>>19みたいな微妙に命題を変形するようなのは楽に書けるようにしたい
24/04/19 12:06:54.47 0YEF9E1Q.net
まず代数計算は自動化したいよね
ほぼ定義を再掲するだけみたいな証明は自動で演繹できるようにしたい
全部が全部そうできなくてもいいけど、書き方に若干のルールを設ければ自動で証明できる範囲は広がるはず
型駆動でも、OOPでいうとこのデザインパターンを発見して、
>>10や>>19みたいな微妙に命題を変形するようなのは楽に書けるようにしたい