A.3 Declarations
In this section, we describe the language's declaration expressions
denoting declarations each of which extends the environment by a
mapping of an identifier to a type, value, or formula. When type checking a
declaration, a type checking condition may be generated which is
forwarded to a decision procedure for automatic proving. If the condition
cannot be proved, a warning is issued, but the type checking condition is
nevertheless assumed true. Thus the user must establish by a separate
proof that the type checking condition is valid (any further proof
might be unsound, otherwise).
Wolfgang
Schreiner