はどんなに頑張ってもだめだったので、 を試してみた。 すなわち match t1, t2, t3, t4, t5, t6, t7 with | Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, Node s1 s2 => f_2 s1 s2 | s1, s2, s3, s4, s5, s6, s7 => Node s1 (Node s2 (Node s3 (Node s4 (Node s5 (N…

とにかく、デフォルトの場合にまとめられるところをまとめるという考えでいくと match t1, t2, t3, t4, t5, t6, t7 with | 特殊な場合 => | s1, s2, s3, s4, s5, s6, s7 => Node s1 (Node s2 (Node s3 (Node s4 (Node s5 (Node s6 s7))))) endとするのがよい…

最初の場合わけ match t1, t2, t3, t4, t5, t6, t7 with | Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, s1 => f_1 s1 (* T *) | Leaf, Leaf, Leaf, Leaf, Leaf, (Node s1 s2), s3 => f_3 s1 s2 s3 (* T^3 *) | Leaf, Leaf, Leaf, Leaf, (Node s1 s2), s3, s4 => f_…

http://d.hatena.ne.jp/m-hiyama/20081031

Inductive Tree : Set := | Leaf | Node : Tree -> Tree -> Tree. Inductive Tree7 : Set := | T7 : Tree -> Tree -> Tree -> Tree -> Tree -> Tree -> Tree -> Tree7. Definition f (ts : Tree7) : Tree := match ts with | T7 Leaf Leaf Leaf Leaf Leaf Le…