@zwarich @MartinEscardo For positivity checking we need to check how definitions and arguments occur in definitions. We do this for a mutual block at once. The old code used a naive cubic transitive closure of the occurrence graph. The new code is a quadratic depth-first search that's more specific for the work and also more optimized. https://github.com/agda/agda/commit/4e481bf79340e0e58a99818e20dbf377d1acae90