On 11/02/2015, at 4:53 pm, Kim-Ee Yeoh wrote:
I think Roman defines "depth" that way because it counts the total number of constructors (i.e. tree nodes) in the path.
That is a perfectly reasonable thing to count, but "depth" is not a good name for it.