[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 07/01/2018 17:41, Xavier Leroy wrote: > As your example shows, the tree can contain infinitely-branching nodes, hence > the size can be infinite, but all paths are finite, hence the height is > finite. I was confused. All paths in this tree are finite indeed, and that's why it induces a well-founded ordering. But in the presence of infinitely-branching nodes, the height can still be infinite and is not an appropriate justification for structural induction. Sorry for the noise, - Xavier Leroy
