|
|
|---|
|
|
|
|---|
Struct type recursion checks in Leo.
Struct types may contain components with other struct types, but there cannot be any circularity: a struct type cannot include, directly or indirectly, components of the same struct type. If such a circularity existed, it would be impossible to construct values of the struct type, because values in Leo are finite objects.
Thus, the Leo static semantics includes the requirement that there is no recursion in struct types (in the sense above). Here we formalize this requirement, by constructing a dependency graph among type identifiers and ensuring that there are no circularities in the graph.