2012-04-02から1日間の記事一覧

Ltac と proof term 5

tactic が proof term を生成していく様子を何度か観察しましたが,何のためにそんなことをしていたかというと,ときどき tactic が失敗してよくわからないエラーを出すことがあるのでその理由を知りたかったのです。今回はそこに近づこうとしてみます。例と…