Certain details are ignored, such as the interpretation of type expressions, which is straightforward in Iota in any case. M is well-typed. This environment construction is performed by the function module-env , which is defined below. In this rule, brackets are placed around the definition D to distinguish the judgment that a declaration is type-safe from other judgments that the static checker makes. The function module-env performs the gathering of information about variables and functions that are visible at the top level, and can be defined recursively.
Function definitions are less trivial.
These rules say that to check the type safety of a function definition, we check that the expression E that is the body of the function has the expected type T r that is the declared return type of the function. In the case of a function that does not return a value, the expression E may have any type T r . The type of the expression E is determined in an environment that includes all of the argument variables a i of the function, bound to their corresponding types T i , which is necessary because E may mention these variables. The addition of two environments is the union of those environments as long as the two environments do not contain any definitions with the same name. If two environments contain definitions with the same name, the addition of the environments is undefined.