On Sun, Jan 17, 2016 at 10:17 AM, 鲍凯文
necessary? I found this: http://ssomayyajula.github.io/posts/2015-11-07-proofs-of-functor-laws-with-H..., which goes over an inductive (on the length of the list) proof for the list type, but I'm not sure how to do it for a Tree.
You've got the right idea. The general outline of a simple inductive proof is this: 1. Prove for the smallest case (in this case, a tree with just one Leaf) 2. While assuming that the hypothesis holds for a small case, prove hypothesis for the next case one up in size 3. Put 1 and 2 together to claim hypothesis for all cases You've done 1. You're stuck at 2 because you haven't yet found some measure of a "size" of a Tree. What are some common Tree measures you've seen? -- Kim-Ee