[TYPES] Statement of structural induction

[Xavier Leroy]

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