Function recursion checks in Leo.
Functions may call other functions, but currently any kind of (direct or indirect) recursion is prohibited. Some forms of bounded recursion may be allowed in the future, but for now that is not the case.
Thus, the Leo static semantics includes the requirement that there is no function recursion. Here we formalize this requirement, by constructing a dependency graph among the functions and ensuring that there are no circularities in the graph.