Agda.Termination.RecCheck

Checking for recursion:

• We detect truly (co)recursive definitions by computing the dependency graph and checking for cycles.
• This is inexpensive and let us skip the termination check when there's no (co)recursion

Original contribution by Andrea Vezzosi (sanzhiyan). This implementation by Andreas.

Documentation

recursive :: [QName] -> TCM [[QName]]

Given a list of formally mutually recursive functions, check for actual recursive calls in the bodies of these functions. Returns the actually recursive functions as strongly connected components.

As a side effect, update the clauseRecursive field in the clauses belonging to the given functions.

anyDefs :: GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)

anysDef names a returns all definitions from names that are used in a.