An integer that, for each of the given sequences, is equal to the sequence's length.

This is treated as an IndexOrHigh annotation internally. This is an implementation detail that may change in the future, when this type may be used to implement more precise refinements.

The usual use case for the LengthOf annotation is in the defintions of custom collections. Consider the signature of java.lang.String#length():

    public @LengthOf("this") int length()