いや、プロシンのネタにしようと思って... ってことは、これから書くんですか? 8月くらいからやってるんですが...
こういうのって、やってると広がって、あれもこれもやりたいになるのだが...
Agda なので時間がかかる
かかる割に、システム更新とか授業とか他のもろもろとか... 事務は可能な限りさぼってるのに。
要は順列を数え上げて「全部数え上げたことを確認すれば良い」だけなんですが、割と迷走中。
でも、ある程度は形にはなったかな。Agdaの証明つまり型の整合を見るのに4分かかるのが10秒になるみたいな話らしいです。
え、そこ速度見るの?
No comments:
Post a Comment