Pragma Type_Invariant (GNAT Reference Manual)

### 2.190 Pragma Type_Invariant ¶

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.