Syntax:
pragma Type_Invariant ([Entity =>] type_LOCAL_NAME, [Check =>] EXPRESSION);
The Type_Invariant pragma is intended to be an exact
replacement for the language-defined Type_Invariant
aspect, and shares its restrictions and semantics. It differs
from the language defined Invariant pragma in that it
does not permit a string parameter, and it is
controlled by the assertion identifier Type_Invariant
rather than Invariant.
This is an assertion kind pragma that can associate a set of its arguments with an assertion level. See SPARK 2014 Reference Manual, section 11.4.2.