https://twitter.com/kinaba のログ (twilog の方が便利です。)
| 心のおもむくままに書いていたらどうしようもないことになった…頭が悪すぎる… http://as305.dyndns.org/aps/problem/view/6 | |
| Coqの { A }+{ B } や _ + { _ } ってどういう意味だっけ。∨をProp以外に一般化したみたいな感じかな。Aの元であるかBの元であるかどっちかとその証拠 | |
| 書いてあった http://www.lix.polytechnique.fr/coq/stdlib/Coq.Init.Specif.html "boolean type equipped with the justification of their value" |