#Basics-J.agdaのandb-true-elim2
#c == trueを証明したいのでcに対してCase分けしてみたんだけど
#andb-true-elim2 b true eq = refl
#andb-true-elim2 b false ()
#これだと()がyellowになる
#if some meta-variable other than the goals cannot be solved the code will be highlighted in yellow
#target以外のメタ変数を解決できない場合にyelloにハイライトされる
#ってことなんだけどbをさらにCase分けしないといけないっぽいんだが(Basics-Jの回答からすると)、
#これはagdaとしては何をしようとして問題になってるの？
#andb-true-elim1ではcのCase分けが不要っぽいんだけどそっちはなぜCase分け不要なの？
#あとこれも似たようなところが分かってないんだろうけど
##例のchallengeのFibonacci functionですが、Basics-Jでplus-commが出てきたのでrewriteを使えばできるじゃんと思ってやってみたんですが、これだとtermination checkでerrorになります.
#notogawaさんの回答みたいにsubstにあたるものが要るのかもしれませんが、それとは別にそもそもこれでなぜ停止性判定がアウトになるのかわかりません。
#これはf (suc (suc n)) => f (suc n) とf nとに再帰しているけど、これはいずれも減じる方向だから停止するのでは？
haskell-ja > Archives > 2013/06/03