Comment by aatd86

Why doesn't it seem exactly true?

It is an integer. It is in the definition. And any value should be equal to nine. By construction Nine could have been given the same representation as int, at first. Except this is not enough to express the refinement/proposition.

One could represent it as a fat pointer with a space allocated to the set of propositions/predicates to check the value of.

That allows to check for equality for instance.

That information would not be discarded.

This is basically a subtype of int.

As such, it is both a dependent type and a refinement type. While it is true that not all refinement types are dependent types, because of cardinality.

I think Maxatar response in the same thread puts it in words that are possibly closer to the art.