2013-07-20から1日間の記事一覧
昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。なんかこういうのを考えていて, Inductive mov : nat -> nat -> Prop := | mov_1 : forall m, mov (S m) m | mov_2 : forall m, mov…
昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。なんかこういうのを考えていて, Inductive mov : nat -> nat -> Prop := | mov_1 : forall m, mov (S m) m | mov_2 : forall m, mov…