- 2012-10-17 (Wed) 23:37
- 一般
まあ，exists x とか書かれていたとして具体的にどれが出てくるかとか証明上は関係ないのだから何かを取り出そうとしないというのが自然な思考なのだけど，ときどき値が取り出せたらなぁと思わなくない．
とりあえず Prop の扱いにまだ慣れていないらしい．
閑話休題．
証明を対話的にやるのが面倒だから直接プログラム書いてしまえと思うようになってきた．が，まだ tactic と実際のコードとの対応とかが把握しきれていないのでなんとも難しい．
- Newer: ことはじめ